moved initial (i.e. empty) lexiconEngine status to lexiconEngine from

lexiconSync

diff --git a/helm/software/components/grafite_parser/cicNotation2.ml b/helm/software/components/grafite_parser/cicNotation2.ml
index 015d426e72c82acde6b4509b1a57cb41d097b58b..b3c8a59cc81231a44c49ccf102e809fe4bf7f1a4 100644 (file)
--- a/helm/software/components/grafite_parser/cicNotation2.ml
+++ b/helm/software/components/grafite_parser/cicNotation2.ml
@@ -28,7 +28,7 @@
 let load_notation ~include_paths fname =
   let ic = open_in fname in
   let lexbuf = Ulexing.from_utf8_channel ic in
-  let status = ref LexiconSync.init in
+  let status = ref LexiconEngine.initial_status in
   try
    while true do
     status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status)
@@ -38,7 +38,7 @@ let load_notation ~include_paths fname =
 
 let parse_environment ~include_paths str =
  let lexbuf = Ulexing.from_utf8_string str in
- let status = ref LexiconSync.init in
+ let status = ref LexiconEngine.initial_status in
  try
   while true do
    status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status)

diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml
index aec759c964d64d3b3d00f9ea92d87c73d42a5445..4adfe624b2039c4042e925a6ed2641e1c0b37c98 100644 (file)
--- a/helm/software/components/lexicon/lexiconEngine.ml
+++ b/helm/software/components/lexicon/lexiconEngine.ml
@@ -36,6 +36,14 @@ type status = {
   metadata: LibraryNoDb.metadata list;
 }
 
+let initial_status = {
+  aliases = DisambiguateTypes.Environment.empty;
+  multi_aliases = DisambiguateTypes.Environment.empty;
+  lexicon_content_rev = [];
+  notation_ids = [];
+  metadata = [];
+}
+
 let add_lexicon_content cmds status =
   let content = status.lexicon_content_rev in
   let content' =

diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli
index ba09386402cd110b437d8d95437b8c8b8e413ab0..8e8b420ba03fabc9354a784b835e7313db38c3b9 100644 (file)
--- a/helm/software/components/lexicon/lexiconEngine.mli
+++ b/helm/software/components/lexicon/lexiconEngine.mli
@@ -33,9 +33,12 @@ type status = {
   metadata: LibraryNoDb.metadata list;
 }
 
+val initial_status: status
+
 val eval_command : status -> LexiconAst.command -> status
 
 val set_proof_aliases:
  status ->
   (DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) list ->
   status
+

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index d7fa27f902b2e7038ee46e7b3c9ed9986e025b47..f88a79971b32919e0441a31f85bf8999840376bd 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -109,11 +109,3 @@ let time_travel ~present ~past =
   in
    List.iter CicNotation.remove_notation notation_to_remove
 
-let init =
-  {
-    LexiconEngine.aliases = DisambiguateTypes.Environment.empty;
-    multi_aliases = DisambiguateTypes.Environment.empty;
-    lexicon_content_rev = [];
-    notation_ids = [];
-    metadata = [];
-  }

diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli
index 62d8b97f567b6791111906538cd0e3de0abfcfff..bba152a9f050f020af6cf3ef04066bda43289187 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.mli
+++ b/helm/software/components/lexicon/lexiconSync.mli
@@ -37,4 +37,3 @@ val alias_diff:
  from:LexiconEngine.status -> LexiconEngine.status ->
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list
 
-val init: LexiconEngine.status