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
[], 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
) 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
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
| 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
is_there_and_executable s
with
| CicNotationParser.Parse_error _ -> false
- | Margin -> true
-
-
-
+ | Margin | End_of_file -> true
+
(* debug *)
method dump () =
MatitaLog.debug "script status:";