From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 22 Feb 2006 22:39:47 +0000 (+0000)
Subject: moved initial (i.e. empty) lexiconEngine status to lexiconEngine from
X-Git-Tag: make_still_working~7536
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=004fbb54bc0a2b971f08bcf830ac8cbdafcdbe57;p=helm.git

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 015d426e7..b3c8a59cc 100644
--- 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 aec759c96..4adfe624b 100644
--- 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 ba0938640..8e8b420ba 100644
--- 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 d7fa27f90..f88a79971 100644
--- 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 62d8b97f5..bba152a9f 100644
--- 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