fixed coercions undoooing

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4c53f113bd9d0db4b7707d628a320be84f00dee8..4b1b994d97f8e01b22278d1a787fd084da688be1 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -36,6 +36,7 @@ let debug_print = if debug then prerr_endline else ignore
   (** raised when one of the script margins (top or bottom) is reached *)
 exception Margin
 exception NoUnfinishedProof
+exception ActionCancelled
 
 let safe_substring s i j =
   try String.sub s i j with Invalid_argument _ -> assert false
@@ -140,27 +141,24 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
    in
     res,parsed_text_length
 
-let eval_with_engine
-     guistuff lexicon_status grafite_status user_goal parsed_text st
-=
-  try
-   eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text
-    st
+let wrap_with_developments guistuff f arg = 
+  try 
+    f arg
   with
   | DependenciesParser.UnableToInclude what 
+  | LexiconEngine.IncludedFileNotCompiled what 
   | GrafiteEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
-        let target = what in
+        let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in
         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 lexicon_status grafite_status user_goal
-          parsed_text st
+          f arg
       in
-      let do_nothing () = [], 0 in
+      let do_nothing () = raise ActionCancelled in
       let handle_with_devel d =
         let name = MatitamakeLib.name_for_development d in
         let title = "Unable to include " ^ what in
@@ -198,6 +196,14 @@ let eval_with_engine
           | None -> handle_without_devel (Some f)
           | Some d -> handle_with_devel d
 ;;
+    
+let eval_with_engine
+     guistuff lexicon_status grafite_status user_goal parsed_text st
+=
+  wrap_with_developments guistuff
+    (eval_with_engine 
+      guistuff lexicon_status grafite_status user_goal parsed_text) st
+;;
 
 let pp_eager_statement_ast =
   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
@@ -352,8 +358,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
-        GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
-         ~include_paths lexicon_status, text
+        let ast = 
+          wrap_with_developments guistuff
+            (GrafiteParser.parse_statement 
+              (Ulexing.from_utf8_string text) ~include_paths) lexicon_status 
+        in
+          ast, text
     | `Ast (st, text) -> (lexicon_status, st), text
   in
   let text_of_loc loc =
@@ -770,23 +780,23 @@ object (self)
 
   method eos = 
     let s = self#getFuture in
-    let rec is_there_and_executable lexicon_status s = 
+    let rec is_there_only_comments lexicon_status s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
       let lexicon_status,st =
        GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
         ~include_paths lexicon_status
       in
       match st with
-        GrafiteParser.LNone loc
       | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
           let parsed_text_length = snd (HExtlib.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 lexicon_status next
-      | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false
+          is_there_only_comments lexicon_status next
+      | GrafiteParser.LNone _
+      | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
     in
     try
-      is_there_and_executable self#lexicon_status s
+      is_there_only_comments self#lexicon_status s
     with 
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true