removed no longer used METAs

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index d628af98dff7b237331bb4ca094087a9e41438ec..188726d9510879720ff984782cd5d8e26fe558d6 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
@@ -80,8 +81,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
 =
   let module TAPp = GrafiteAstPp in
   let parsed_text_length = String.length parsed_text in
-  let loc, ex = 
-    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
   let initial_space,parsed_text =
    try
     let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
@@ -91,7 +90,9 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
    (* the code commented out adds the "select" command if needed *)
    initial_space,grafite_status,lexicon_status,[] in
-(*    match grafite_status.proof_status with
+(* let loc, ex = 
+    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
+    match grafite_status.proof_status with
      | Incomplete_proof { stack = stack }
       when not (List.mem user_goal (Continuationals.head_goals stack)) ->
         let grafite_status =
@@ -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 =
@@ -499,7 +509,9 @@ object (self)
       bottom) and we will face a macro *)
    match self#grafite_status.proof_status with
       Incomplete_proof p ->
-       userGoal <- Some (Continuationals.Stack.find_goal p.stack)
+       userGoal <-
+         (try Some (Continuationals.Stack.find_goal p.stack)
+         with Failure _ -> None)
     | _ -> userGoal <- None
 
   method private _retract offset lexicon_status grafite_status new_statements
@@ -755,9 +767,8 @@ object (self)
 
   method proofContext =
    match userGoal with
-      None -> assert false
-    | Some n ->
-       GrafiteTypes.get_proof_context self#grafite_status n
+      None -> []
+    | Some n -> GrafiteTypes.get_proof_context self#grafite_status n
 
   method proofConclusion =
    match userGoal with
@@ -766,28 +777,28 @@ object (self)
        GrafiteTypes.get_proof_conclusion self#grafite_status n
 
   method stack = GrafiteTypes.get_stack self#grafite_status
-  method setGoal n = userGoal <- Some n
+  method setGoal n = userGoal <- n
   method goal = userGoal
 
   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