@@ -11,10 +11,11 @@ import type { ValidatedModel } from "./model_library";
1111export type ModelDocument = Document & { type : "model" } ;
1212
1313/** Create an empty model document. */
14- export const newModelDocument = ( theory : string ) : ModelDocument => ( {
14+ export const newModelDocument = ( theory : string , editorVariant ?: string ) : ModelDocument => ( {
1515 name : "" ,
1616 type : "model" ,
1717 theory,
18+ ...( editorVariant ? { editorVariant } : { } ) ,
1819 notebook : newNotebook < ModelJudgment > ( ) ,
1920 version : currentVersion ( ) ,
2021} ) ;
@@ -57,37 +58,72 @@ export async function createModel(
5758 return api . createDoc ( init ) ;
5859}
5960
60- /** Migrate a model document from one theory to another. */
61- export async function migrateModelDocument (
61+ /** Migrate a model document to a different theory, or switch its editor variant.
62+ */
63+ export async function switchTheoryOrEditor (
6264 liveModel : LiveModelDoc ,
63- targetTheoryId : string ,
65+ editorOrModelId : string ,
6466 theories : TheoryLibrary ,
6567) {
6668 const { doc, changeDoc } = liveModel . liveDoc ;
67- const targetTheory = await theories . get ( targetTheoryId ) ;
69+
70+ let targetBaseId : string = editorOrModelId ;
71+ let targetEditorVariant : string | undefined ;
72+ const isEditor = theories . isEditorVariant ( editorOrModelId ) ;
73+ if ( isEditor ) {
74+ const base = theories . getBaseTheoryId ( editorOrModelId ) ;
75+ invariant ( base !== undefined , "Editor variant must have a base theory" ) ;
76+ targetBaseId = base ;
77+ targetEditorVariant = editorOrModelId ;
78+ }
79+
80+ // If only the editor variant is changing (same base theory), just flip the field.
81+ if ( targetBaseId === doc . theory ) {
82+ changeDoc ( ( doc ) => {
83+ if ( targetEditorVariant ) {
84+ doc . editorVariant = targetEditorVariant ;
85+ } else {
86+ delete doc . editorVariant ;
87+ }
88+ } ) ;
89+ return ;
90+ }
91+
92+ // Real theory migration below.
93+ const targetTheory = await theories . get ( targetBaseId ) ;
6894 const theory = liveModel . theory ( ) ;
6995 let model = liveModel . elaboratedModel ( ) ;
7096 invariant ( theory && model ) ; // FIXME: Should fail gracefully.
7197
7298 // Trivial migration.
73- if ( ! NotebookUtils . hasFormalCells ( doc . notebook ) || theory . inclusions . includes ( targetTheoryId ) ) {
99+ if ( ! NotebookUtils . hasFormalCells ( doc . notebook ) || theory . inclusions . includes ( targetBaseId ) ) {
74100 changeDoc ( ( doc ) => {
75- doc . theory = targetTheoryId ;
101+ doc . theory = targetBaseId ;
102+ if ( targetEditorVariant ) {
103+ doc . editorVariant = targetEditorVariant ;
104+ } else {
105+ delete doc . editorVariant ;
106+ }
76107 } ) ;
77108 return ;
78109 }
79110
80111 // Pushforward migration.
81- const migration = theory . pushforwards . find ( ( m ) => m . target === targetTheoryId ) ;
112+ const migration = theory . pushforwards . find ( ( m ) => m . target === targetBaseId ) ;
82113 if ( ! migration ) {
83- throw new Error ( `No migration defined from ${ theory . id } to ${ targetTheoryId } ` ) ;
114+ throw new Error ( `No migration defined from ${ theory . id } to ${ targetBaseId } ` ) ;
84115 }
85116 // TODO: We need a general method to propagate changes from catlog models to
86117 // notebooks. This stop-gap solution only works because pushforward
87118 // migration doesn't have to create/delete cells, only update types.
88119 model = migration . migrate ( model , targetTheory . theory ) ;
89120 changeDoc ( ( doc ) => {
90- doc . theory = targetTheoryId ;
121+ doc . theory = targetBaseId ;
122+ if ( targetEditorVariant ) {
123+ doc . editorVariant = targetEditorVariant ;
124+ } else {
125+ delete doc . editorVariant ;
126+ }
91127 for ( const judgment of NotebookUtils . getFormalContent ( doc . notebook ) ) {
92128 if ( judgment . tag === "object" ) {
93129 judgment . obType = model . obType ( {
0 commit comments