X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=52d18f42a3ea5d43caaf6856d02d5aabb8377900;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=3beadf1fe185d4cae798b3bd3900c3f3564164fb;hpb=e465656be7e67ee3c02acf12a53c8388ae384b0a;p=helm.git

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 3beadf1fe..52d18f42a 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -34,23 +34,21 @@ exception AttemptToInsertAnAlias
 
 (** {2 Initialization} *)
 
-let grafite_status = (ref None : GrafiteTypes.status option ref)
-let lexicon_status = (ref None : LexiconEngine.status option ref)
+let grafite_status = (ref [] : GrafiteTypes.status list ref)
 
 let run_script is eval_function  =
-  let lexicon_status',grafite_status' = 
-    match !lexicon_status,!grafite_status with
-    | Some ss, Some 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 := Some lexicon_status'';
-       grafite_status := Some grafite_status''
+    | (grafite_status'',None)::_ ->
+       grafite_status := grafite_status''::!grafite_status
     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
   with
   | GrafiteEngine.Drop  
@@ -63,81 +61,149 @@ let run_script is eval_function  =
       raise exn
 
 let clean_exit n =
- let opt_exit =
-  function
-     None -> ()
-   | Some n -> exit n
- in
   match !grafite_status with
-     None -> opt_exit n
-   | Some grafite_status ->
-      try
-       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+     [] -> exit n
+   | grafite_status::_ ->
+       let baseuri = grafite_status#baseuri in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
-       opt_exit n
-      with GrafiteTypes.Option_error("baseuri", "not found") ->
-       (* no baseuri ==> nothing to clean yet *)
-       opt_exit n
+       exit n
 
-let terminate () =
+let terminate n =
  let terminator = String.make 1 (Char.chr 249) in
-  print_endline terminator;
-  prerr_endline terminator
+ let prompt =
+  (match n with
+     None -> "-1"
+   | Some n -> string_of_int n) ^ terminator
+ in
+  print_endline prompt;
+  prerr_endline prompt
+;;
+
+let outer_syntax_parser () =
+ let text = ref "" in
+ let tag = ref `Do in
+ let callbacks =
+  { XmlPushParser.default_callbacks with
+    XmlPushParser.start_element =
+     (Some
+       (fun name attrs ->
+         match name with
+            "pgip" -> ()
+          | "doitem" -> tag := `Do
+          | "undoitem" -> tag := `Undo
+          | _ -> assert false)) ;
+    XmlPushParser.character_data =
+     (Some (fun s -> text := !text ^ s)) ;
+    XmlPushParser.end_element =
+     (Some
+       (function
+           "pgip" -> raise (XmlPushParser.Parse_error "EOC")
+         | "doitem"
+         | "undoitem" -> ()
+         | _ -> assert false))
+  }
+ in
+  let parse = XmlPushParser.create_parser callbacks in
+    try
+     XmlPushParser.parse parse (`Channel stdin) ;
+     raise End_of_file
+    with
+       XmlPushParser.Parse_error "no element found" -> raise End_of_file
+     | XmlPushParser.Parse_error "EOC" ->
+        match !tag with
+           `Do -> `Do !text
+         | `Undo ->
+             try
+              `Undo (int_of_string !text)
+             with
+              Failure _ -> assert false
+;;
+
+let include_paths =
+ lazy (Helm_registry.get_list Helm_registry.string "matita.includes")
 ;;
   
 let rec interactive_loop () = 
   (* every loop is terminated by a terminator both on stdout and stderr *)
-  let interactive_loop () = terminate(); interactive_loop () in
-  let str = Ulexing.from_utf8_channel stdin in
-  let watch_statuses lexicon_status grafite_status =
-   match grafite_status.GrafiteTypes.proof_status with
-      GrafiteTypes.Incomplete_proof
-       {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
-        GrafiteTypes.stack = stack } ->
-        let open_goals = Continuationals.Stack.open_goals stack in
-        print_endline
-         (String.concat "\n"
-           (List.map
-             (fun i ->
-               ApplyTransformation.txt_of_cic_sequent 80 metasenv
-                (List.find (fun (j,_,_) -> j=i) metasenv)
-             ) open_goals))
-    | _ -> ()
-  in
-  let include_paths =
-   Helm_registry.get_list Helm_registry.string "matita.includes" in
+  let interactive_loop n = terminate n; interactive_loop () in
   try
-    run_script str 
-      (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
-      ~include_paths ~watch_statuses) ;
-    interactive_loop ()
+   match outer_syntax_parser () with
+      `Undo n ->
+        let rec drop =
+         function
+            0,l -> l
+          | n,_::l -> drop (n-1,l)
+          | _,[] -> assert false
+        in
+         let to_be_dropped = List.length !grafite_status - n in
+         let safe_hd = function [] -> assert false | he::_ -> he in
+         let cur_grafite_status = safe_hd !grafite_status in
+          grafite_status := drop (to_be_dropped, !grafite_status) ;
+          let grafite_status = safe_hd !grafite_status in
+           LexiconSync.time_travel
+            ~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 grafite_status =
+         match grafite_status#proof_status with
+            GrafiteTypes.Incomplete_proof
+             {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
+              GrafiteTypes.stack = stack } ->
+              let open_goals = Continuationals.Stack.open_goals stack in
+              print_endline
+               (String.concat "\n"
+                 (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 
+           ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
+         interactive_loop (Some (List.length !grafite_status))
   with 
-  | GrafiteEngine.Macro (floc,_) ->
-     let x, y = HExtlib.loc_of_floc floc in
-      HLog.error
-       (sprintf "A macro has been found in a script at %d-%d" x y);
-      interactive_loop ()
-  | Sys.Break -> HLog.error "user break!"; interactive_loop ()
-  | GrafiteTypes.Command_error _ -> interactive_loop ()
-  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
-     let x, y = HExtlib.loc_of_floc floc in
-      HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
-      interactive_loop ()
-  | End_of_file as exn -> raise exn
-  | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
+   | GrafiteEngine.Macro (floc,_) ->
+      let x, y = HExtlib.loc_of_floc floc in
+       HLog.error
+        (sprintf "A macro has been found in a script at %d-%d" x y);
+       interactive_loop None
+   | Sys.Break -> HLog.error "user break!"; interactive_loop None
+   | GrafiteTypes.Command_error _ -> interactive_loop None
+   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+      let x, y = HExtlib.loc_of_floc floc in
+       HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+       interactive_loop None
+   | End_of_file as exn -> raise exn
+   | exn -> HLog.error (Printexc.to_string exn); interactive_loop None
 
 
 let main () = 
   MatitaInit.initialize_all ();
+  HLog.set_log_callback
+   (fun tag msg ->
+     let s =
+      match tag with
+         `Debug -> "<div style='color:blue'>Debug: " ^ msg ^ "</div><br/>\n"
+       | `Message -> "<div style='color:green'>Info: " ^ msg ^ "</div><br/>\n"
+       | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
+       | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
+     in
+      output_string stderr s;
+      flush stderr
+   );
   (* 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 := Some (GrafiteSync.init ());
-  lexicon_status :=
-   Some (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
@@ -153,28 +219,28 @@ let main () =
       interactive_loop ()
      with
       | End_of_file -> ()
-      | GrafiteEngine.Drop -> clean_exit (Some 1)
+      | GrafiteEngine.Drop -> clean_exit 1
     );
-    let proof_status,moo_content_rev,metadata,lexicon_content_rev = 
-      match !lexicon_status,!grafite_status with
-      | Some ss, Some s ->
-         s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
-          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
       HLog.error
        "there are still incomplete proofs at the end of the script";
-      clean_exit (Some 2)
+      clean_exit 2
      end
     else
      begin
        let baseuri =
-        GrafiteTypes.get_string_option
-         (match !grafite_status with
-             None -> assert false
-           | Some 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 
@@ -183,16 +249,12 @@ let main () =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       let metadata_fname =
-        LibraryMisc.metadata_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true
-       in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LibraryNoDb.save_metadata metadata_fname metadata;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+       NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with 
   | exn ->
       if matita_debug then raise exn;
-      clean_exit (Some 3)
+      clean_exit 3