Estatus finally merged into the global status using inheritance.

[helm.git] / helm / software / matita / matitaWiki.ml

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index bbe8d2ed7247f60132ffa0f97e4c7e298959efc9..f9c9af3590de8cdb03a1ba1f6dde67f4e7a18ef1 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -35,21 +35,19 @@ exception AttemptToInsertAnAlias
 (** {2 Initialization} *)
 
 let grafite_status = (ref [] : GrafiteTypes.status list ref)
-let lexicon_status = (ref [] : LexiconEngine.status list ref)
 
 let run_script is eval_function  =
-  let lexicon_status',grafite_status' = 
-    match !lexicon_status,!grafite_status with
-    | ss::_, s::_ -> ss,s
-    | _,_ -> assert false
+  let grafite_status' = 
+    match !grafite_status with
+    | s::_ -> s
+    | _ -> assert false
   in
   let cb = fun _ _ -> () in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   try
-   match eval_function lexicon_status' grafite_status' is cb with
+   match eval_function grafite_status' is cb with
       [] -> raise End_of_file
-    | ((grafite_status'',lexicon_status''),None)::_ ->
-       lexicon_status := lexicon_status''::!lexicon_status;
+    | (grafite_status'',None)::_ ->
        grafite_status := grafite_status''::!grafite_status
     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
   with
@@ -66,13 +64,9 @@ let clean_exit n =
   match !grafite_status with
      [] -> exit n
    | grafite_status::_ ->
-      try
-       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+       let baseuri = grafite_status#baseuri in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
        exit n
-      with GrafiteTypes.Option_error("baseuri", "not found") ->
-       (* no baseuri ==> nothing to clean yet *)
-       exit n
 
 let terminate n =
  let terminator = String.make 1 (Char.chr 249) in
@@ -141,23 +135,20 @@ let rec interactive_loop () =
           | n,_::l -> drop (n-1,l)
           | _,[] -> assert false
         in
-         let to_be_dropped = List.length !lexicon_status - n in
+         let to_be_dropped = List.length !grafite_status - n in
          let safe_hd = function [] -> assert false | he::_ -> he in
-         let cur_lexicon_status = safe_hd !lexicon_status in
          let cur_grafite_status = safe_hd !grafite_status in
-          lexicon_status := drop (to_be_dropped, !lexicon_status) ;
           grafite_status := drop (to_be_dropped, !grafite_status) ;
-          let lexicon_status = safe_hd !lexicon_status in
           let grafite_status = safe_hd !grafite_status in
            LexiconSync.time_travel
-            ~present:cur_lexicon_status ~past:lexicon_status;
+            ~present:cur_grafite_status ~past:grafite_status;
            GrafiteSync.time_travel
             ~present:cur_grafite_status ~past:grafite_status;
            interactive_loop (Some n)
     | `Do command ->
         let str = Ulexing.from_utf8_string command in
-        let watch_statuses lexicon_status grafite_status =
-         match grafite_status.GrafiteTypes.proof_status with
+        let watch_statuses grafite_status =
+         match grafite_status#proof_status with
             GrafiteTypes.Incomplete_proof
              {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
               GrafiteTypes.stack = stack } ->
@@ -167,14 +158,16 @@ let rec interactive_loop () =
                  (List.map
                    (fun i ->
                      ApplyTransformation.txt_of_cic_sequent 80 metasenv
+                      ~map_unicode_to_tex:(Helm_registry.get_bool
+                        "matita.paste_unicode_as_tex")
                       (List.find (fun (j,_,_) -> j=i) metasenv)
                    ) open_goals))
           | _ -> ()
         in
          run_script str 
-           (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
+           (MatitaEngine.eval_from_stream ~first_statement_only:true 
            ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
-         interactive_loop (Some (List.length !lexicon_status))
+         interactive_loop (Some (List.length !grafite_status))
   with 
    | GrafiteEngine.Macro (floc,_) ->
       let x, y = HExtlib.loc_of_floc floc in
@@ -207,13 +200,10 @@ let main () =
    );
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
-  Helm_registry.set_int "matita.verbosity" 0;
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
-  grafite_status := [GrafiteSync.init ()];
-  lexicon_status :=
-   [CicNotation2.load_notation ~include_paths
-     BuildTimeConf.core_notation_script] ;
+  grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths
+   (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
   Sys.catch_break true;
   let origcb = HLog.get_log_callback () in
   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
@@ -231,12 +221,12 @@ let main () =
       | End_of_file -> ()
       | GrafiteEngine.Drop -> clean_exit 1
     );
-    let proof_status,moo_content_rev,lexicon_content_rev = 
-      match !lexicon_status,!grafite_status with
-      | ss::_, s::_ ->
-         s.proof_status, s.moo_content_rev,
-          ss.LexiconEngine.lexicon_content_rev
-      | _,_ -> assert false
+    let proof_status,moo_content_rev,lexicon_content_rev,dump = 
+      match !grafite_status with
+      |  s::_ ->
+         s#proof_status, s#moo_content_rev,
+          s#lstatus.LexiconEngine.lexicon_content_rev, s#dump
+      | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
      begin
@@ -247,10 +237,10 @@ let main () =
     else
      begin
        let baseuri =
-        GrafiteTypes.get_string_option
-         (match !grafite_status with
-             [] -> assert false
-           | s::_ -> s) "baseuri" in
+        (match !grafite_status with
+           [] -> assert false
+         | s::_ -> s)#baseuri
+       in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri 
            ~must_exist:false ~baseuri ~writable:true 
@@ -261,6 +251,7 @@ let main () =
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+       NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with