X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=34e0408c598f281aa0d6bee4417bc3ad5493e407;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=080450416feacdcb27e5b62bdf6c8caf7ca80111;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 080450416..34e0408c5 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -214,8 +214,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
 let disambiguate_macro_term term status user_goal =
   let module MD = MatitaDisambiguator in
   let dbd = MatitaDb.instance () in
-  let metasenv = MatitaMisc.get_proof_metasenv status in
-  let context = MatitaMisc.get_proof_context status user_goal in
+  let metasenv = MatitaTypes.get_proof_metasenv status in
+  let context = MatitaTypes.get_proof_context status user_goal in
   let interps =
    MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
     ~universe:(Some status.multi_aliases) term in
@@ -276,7 +276,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       [], parsed_text_length
   (* REAL macro *)
   | TA.Hint loc -> 
-      let proof = MatitaMisc.get_current_proof status in
+      let proof = MatitaTypes.get_current_proof status in
       let proof_status = proof, user_goal in
       let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
       let selected = guistuff.urichooser l in
@@ -304,8 +304,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           ) selected;
           assert false)
   | TA.Check (_,term) ->
-      let metasenv = MatitaMisc.get_proof_metasenv status in
-      let context = MatitaMisc.get_proof_context status user_goal in
+      let metasenv = MatitaTypes.get_proof_metasenv status in
+      let context = MatitaTypes.get_proof_context status user_goal in
       let interps = 
         MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
          ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
@@ -546,7 +546,7 @@ object (self)
     in
     let s = match statement with Some s -> s | None -> self#getFuture in
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
-    aux (`Raw s)
+    (try aux (`Raw s) with End_of_file -> raise Margin)
 
   method private _retract offset status new_statements new_history =
     let cur_status = match history with s::_ -> s | [] -> assert false in
@@ -759,11 +759,11 @@ object (self)
     | Incomplete_proof _ -> true
     | Intermediate _ -> assert false
 
-(*   method proofStatus = MatitaMisc.get_proof_status self#status *)
-  method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
-  method proofContext = MatitaMisc.get_proof_context self#status userGoal
-  method proofConclusion = MatitaMisc.get_proof_conclusion self#status userGoal
-  method stack = MatitaMisc.get_stack self#status
+(*   method proofStatus = MatitaTypes.get_proof_status self#status *)
+  method proofMetasenv = MatitaTypes.get_proof_metasenv self#status
+  method proofContext = MatitaTypes.get_proof_context self#status userGoal
+  method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal
+  method stack = MatitaTypes.get_stack self#status
   method setGoal n = userGoal <- n
   method goal = userGoal
 
@@ -784,10 +784,8 @@ object (self)
       is_there_and_executable s
     with 
     | CicNotationParser.Parse_error _ -> false
-    | Margin -> true
-      
-    
-    
+    | Margin | End_of_file -> true
+
   (* debug *)
   method dump () =
     MatitaLog.debug "script status:";