X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=e0e4227dd1f5709d921b4bd57f3bf8b0df6594dd;hb=ad0292419b0204384ff55c946a6aabb73a47c42b;hp=4f6627fcd7d5035dd5b4ab399ebf8e7f3f05557d;hpb=619a3a478a4f6b0a50782b620009f6a141c30a53;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4f6627fcd..e0e4227dd 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -61,8 +61,8 @@ let prepend_text header base =
 
   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
 let goal_ast n =
-  let module A = TacticAst in
-  let loc = CicAst.dummy_floc in
+  let module A = GrafiteAst in
+  let loc = Disambiguate.dummy_floc in
   A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
 
 type guistuff = {
@@ -74,11 +74,11 @@ type guistuff = {
 }
 
 let eval_with_engine guistuff status user_goal parsed_text st =
-  let module TA = TacticAst in
-  let module TAPp = TacticAstPp in
+  let module TA = GrafiteAst in
+  let module TAPp = GrafiteAstPp in
   let include_ = 
     match guistuff.filenamedata with
-    | _,None -> []
+    | None,None -> []
     | None,Some devel -> [MatitamakeLib.root_for_development devel ]
     | Some f,_ -> 
         match MatitamakeLib.development_for_dir (Filename.dirname f) with
@@ -130,7 +130,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
     if DisambiguateTypes.Environment.is_empty new_aliases then
       parsed_text
     else
-      prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
+      prepend_text (DisambiguatePp.pp_environment new_aliases)
         parsed_text
   in
   let new_text =
@@ -151,7 +151,10 @@ let eval_with_engine guistuff status user_goal parsed_text st =
       let compile_needed_and_go_on d =
         let root = MatitamakeLib.root_for_development d in
         let target = root ^ "/" ^ what in
-        if not(MatitamakeLib.build_development ~target d) then
+        let refresh_cb () = 
+          while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+        in
+        if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
           raise exc
         else
           eval_with_engine guistuff status user_goal parsed_text st
@@ -208,8 +211,8 @@ let disambiguate term status =
  
 let eval_macro guistuff status parsed_text script mac
 =
-  let module TA = TacticAst in
-  let module TAPp = TacticAstPp in
+  let module TA = GrafiteAst in
+  let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
   let module MDB = MatitaDb in
   let module CTC = CicTypeChecker in
@@ -267,7 +270,7 @@ let eval_macro guistuff status parsed_text script mac
          TA.Executable (loc,
           (TA.Tactical (loc, 
             TA.Tactic (loc,
-             TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None))))))
+             TA.Apply (loc, CicNotationPt.Uri (UriManager.string_of_uri uri,None))))))
         in
         let new_status = MatitaEngine.eval_ast status ast in
         let extra_text = 
@@ -323,8 +326,8 @@ let eval_macro guistuff status parsed_text script mac
 
                                 
 let eval_executable guistuff status user_goal parsed_text script ex =
-  let module TA = TacticAst in
-  let module TAPp = TacticAstPp in
+  let module TA = GrafiteAst in
+  let module TAPp = GrafiteAstPp in
   let module MD = MatitaDisambiguator in
   let module ML = MatitacleanLib in
   let parsed_text_length = String.length parsed_text in
@@ -354,14 +357,14 @@ let eval_executable guistuff status user_goal parsed_text script ex =
 
 let rec eval_statement guistuff status user_goal script s =
   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-  let st = CicTextualParser2.parse_statement (Stream.of_string s) in
+  let st = GrafiteParser.parse_statement (Stream.of_string s) in
   let text_of_loc loc =
-    let parsed_text_length = snd (CicAst.loc_of_floc loc) in
+    let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
     let parsed_text = safe_substring s 0 parsed_text_length in
     parsed_text, parsed_text_length
   in
   match st with
-  | TacticAst.Comment (loc,_)-> 
+  | GrafiteAst.Comment (loc,_)-> 
       let parsed_text, parsed_text_length = text_of_loc loc in
       let remain_len = String.length s - parsed_text_length in
       let s = String.sub s parsed_text_length remain_len in
@@ -372,7 +375,7 @@ let rec eval_statement guistuff status user_goal script s =
       | (status, text) :: tl ->
         ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
       | [] -> [], 0)
-  | TacticAst.Executable (loc, ex) ->
+  | GrafiteAst.Executable (loc, ex) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
       eval_executable guistuff  status user_goal parsed_text script ex 
   
@@ -380,13 +383,15 @@ let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
-class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) 
+class script  ~(view: GText.view)
+              ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
               ~urichooser 
               ~develcreator 
               () =
+let buffer = view#buffer in
 object (self)
   val scriptId = fresh_script_id ()
   
@@ -461,14 +466,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
       end;
     self#moveMark (String.length new_text)
 
-  method private _retract () =
-    match statements, history with
-    | last_statement :: _, cur_status :: prev_status :: _ ->
-        MatitaSync.time_travel ~present:cur_status ~past:prev_status;
-        statements <- List.tl statements;
-        history <- List.tl history;
-        self#moveMark (- (String.length last_statement));
-    | _ -> raise Margin
+  method private _retract offset status new_statements new_history =
+   let cur_status = match history with s::_ -> s | [] -> assert false in
+    MatitaSync.time_travel ~present:cur_status ~past:status;
+    statements <- new_statements;
+    history <- new_history;
+    self#moveMark (- offset)
 
   method advance ?statement () =
     try
@@ -480,8 +483,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
 
   method retract () =
     try
-      self#_retract ();
-      self#notify
+      let cmp,new_statements,new_history,status =
+       match statements,history with
+          stat::statements, _::(status::_ as history) ->
+           String.length stat, statements, history, status
+       | [],[_] -> raise Margin
+       | _,_ -> assert false
+      in
+       self#_retract cmp status new_statements new_history;
+       self#notify
     with 
     | Margin -> self#notify
     | exc -> self#notify; raise exc
@@ -511,6 +521,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
         Incomplete_proof (_,goal) -> self#setGoal goal
       | _ -> ()
     end ;
+    let mark_position = buffer#get_iter_at_mark mark in
+    if view#move_mark_onscreen mark then
+     begin
+      buffer#move_mark mark mark_position;
+      view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
+     end;
     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
   method clean_dirty_lock =
@@ -596,6 +612,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     | `Cursor ->
         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
+        let cmp = (locked_iter ())#offset - (cursor_iter ())#offset in
         let forward_until_cursor () = (* go forward until locked > cursor *)
           let rec aux oldpos =
             self#_advance ();
@@ -606,17 +623,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
           in
           aux (getpos ())
         in
-        let rec back_until_cursor () = (* go backward until locked < cursor *)
-          self#_retract ();
-          if (locked_iter ())#compare (cursor_iter ()) > 0 then
-            back_until_cursor ()
+        let rec back_until_cursor len = (* go backward until locked < cursor *)
+         function
+            statements, (status::_ as history) when len <= 0 ->
+             self#_retract (cmp - len) status statements history
+          | statement::tl1, _::tl2 ->
+             back_until_cursor (len - String.length statement) (tl1,tl2)
+          | _,_ -> assert false
         in
-        let cmp = (locked_iter ())#compare (cursor_iter ()) in
         (try
           if cmp < 0 then       (* locked < cursor *)
             (forward_until_cursor (); self#notify)
           else if cmp > 0 then  (* locked > cursor *)
-            (back_until_cursor (); self#notify)
+            (back_until_cursor cmp (statements,history); self#notify)
           else                  (* cursor = locked *)
               ()
         with 
@@ -638,19 +657,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     let s = self#getFuture in
     let rec is_there_and_executable s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      let st = CicTextualParser2.parse_statement (Stream.of_string s) in
+      let st = GrafiteParser.parse_statement (Stream.of_string s) in
       match st with
-      | TacticAst.Comment (loc,_)-> 
-          let parsed_text_length = snd (CicAst.loc_of_floc loc) in
+      | GrafiteAst.Comment (loc,_)-> 
+          let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_and_executable next
-      | TacticAst.Executable (loc, ex) -> false
+      | GrafiteAst.Executable (loc, ex) -> false
     in
     try
       is_there_and_executable s
     with 
-    | CicTextualParser2.Parse_error _ -> false
+    | CicNotationParser.Parse_error _ -> false
     | Margin -> true
       
     
@@ -670,10 +689,10 @@ end
 
 let _script = ref None
 
-let script ~buffer ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
+    ~view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
   in
   _script := Some s;
   s