- ng_refiner:

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index f1b20efe5929eff2ca0cde49d2e4edf8efc01789..d86871963437efbac813b5e63b590f98573af5ff 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -121,7 +121,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
             ctx in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
-          status None ctx menv subst (parsed_text,parsed_text_length,
+          status `XTNone ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
@@ -132,7 +132,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
       let s = NTactics.intros_tac ~names_ref [] script#status in
       let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
       let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
-      [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+      [s, nl ^ "#" ^ String.concat " #" !names_ref], "", parsed_text_length
   | TA.NAutoInteractive (_loc, (None,a)) -> 
       let trace_ref = ref [] in
       let s = NnAuto.auto_tac ~params:(None,a) ~trace_ref script#status in
@@ -140,20 +140,20 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
         try List.assoc "depth" a
         with Not_found -> ""
       in
-      let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+      let trace = "/"^(if int_of_string depth > 1 then depth else "")^" by " in
       let thms = 
         match !trace_ref with
-        | [] -> "{}"
+        | [] -> ""
         | thms -> 
            String.concat ", "  
              (HExtlib.filter_map (function 
-               | NotationPt.NRef r -> Some (NCicPp.r2s true r) 
+               | NotationPt.NRef r -> Some (NCicPp.r2s status true r) 
                | _ -> None) 
              thms)
       in
       let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
       let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
-      [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+      [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length
   | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_executable include_paths (buffer : GText.buffer)
@@ -247,38 +247,22 @@ let source_view =
     ~insert_spaces_instead_of_tabs:true ~tab_width:2
     ~right_margin_position:80 ~show_right_margin:true
     ~smart_home_end:`AFTER
-    ~packing:parent#add_with_viewport
+    ~packing:parent#add
     () in
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
 let similarsymbols_tag_name = "similarsymbolos" in
 let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
- let status = new GrafiteTypes.status baseuri in
+ let status = new MatitaEngine.status baseuri in
  (match current with
-     Some current ->
-      NCicLibrary.time_travel status;
+     Some current -> NCicLibrary.time_travel status;
 (*
       (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate () *)
    | None -> ());
   status
 in
-let read_include_paths file =
- try 
-   let root, _buri, _fname, _tgt = 
-     Librarian.baseuri_of_script ~include_paths:[] file in 
-   let includes =
-    try
-     Str.split (Str.regexp " ") 
-      (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
-    with Not_found -> []
-   in
-   let rc = root :: includes in
-    List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
-  []
-in
 let default_buri = "cic:/matita/tests" in
 let default_fname = ".unnamed.ma" in
 object (self)
@@ -804,6 +788,7 @@ object (self)
     List.iter (fun o -> o status) observers
 
   method activate =
+    NCicLibrary.replace self#status;
     self#notify
 
   method loadFromFile f =
@@ -822,7 +807,7 @@ object (self)
        let f = Librarian.absolutize file in
         tab_label#set_text (Filename.basename f);
         filename_ <- Some f;
-        include_paths_ <- read_include_paths f;
+        include_paths_ <- MatitaEngine.read_include_paths ~include_paths:[] f;
         self#reset_buffer
 
   method set_star b =
@@ -844,12 +829,12 @@ object (self)
   method private _saveToBackupFile () =
     if buffer#modified then
       begin
-        let f = self#filename in
+        let f = self#filename ^ "~" in
         let oc = open_out f in
         output_string oc (buffer#get_text ~start:buffer#start_iter
                             ~stop:buffer#end_iter ());
         close_out oc;
-        HLog.debug ("backup " ^ f ^ " saved")                    
+        HLog.debug ("backup " ^ f ^ " saved")
       end
   
   method private reset_buffer =