(** raised when one of the script margins (top or bottom) is reached *)
exception Margin
+exception NoUnfinishedProof
let safe_substring s i j =
try String.sub s i j with Invalid_argument _ -> assert false
[], parsed_text_length
(* REAL macro *)
| TA.Hint loc ->
+ let user_goal' =
+ match user_goal with
+ Some n -> n
+ | None -> raise NoUnfinishedProof
+ in
let proof = GrafiteTypes.get_current_proof grafite_status in
- let proof_status = proof,user_goal 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
(match selected with
assert false)
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- let context = GrafiteTypes.get_proof_context grafite_status user_goal in
+ let context =
+ match user_goal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context grafite_status n in
let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
with
MatitaTypes.Cancel -> [], 0
| GrafiteEngine.Macro (_loc,lazy_macro) ->
- let grafite_status,macro = lazy_macro user_goal in
+ let context =
+ match user_goal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+ let grafite_status,macro = lazy_macro context in
eval_macro buffer guistuff lexicon_status grafite_status user_goal
unparsed_text parsed_text script macro
* Invariant: this list length is 1 + length of statements *)
(** goal as seen by the user (i.e. metano corresponding to current tab) *)
- val mutable userGoal = ~-1
+ val mutable userGoal = None
(** text mark and tag representing locked part of a script *)
val locked_mark =
method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false
method private _advance ?statement () =
- let rec aux st =
- let (entries, parsed_len) =
- eval_statement buffer guistuff self#lexicon_status self#grafite_status
- userGoal self st
- in
- let new_statuses, new_statements =
- let statuses, texts = List.split entries in
- statuses, texts
- in
- history <- new_statuses @ history;
- statements <- new_statements @ statements;
- let start = buffer#get_iter_at_mark (`MARK locked_mark) in
- let new_text = String.concat "" (List.rev new_statements) in
- if statement <> None then
- buffer#insert ~iter:start new_text
- else begin
- let s = match st with `Raw s | `Ast (_, s) -> s in
- if new_text <> String.sub s 0 parsed_len then begin
- buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
- buffer#insert ~iter:start new_text;
- end;
- end;
- self#moveMark (String.length new_text)
- in
- let s = match statement with Some s -> s | None -> self#getFuture in
- HLog.debug ("evaluating: " ^ first_line s ^ " ...");
- (try aux (`Raw s) with End_of_file -> raise Margin)
+ let s = match statement with Some s -> s | None -> self#getFuture in
+ HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let (entries, parsed_len) =
+ try
+ eval_statement buffer guistuff self#lexicon_status self#grafite_status
+ userGoal self (`Raw s)
+ with End_of_file -> raise Margin
+ in
+ let new_statuses, new_statements =
+ let statuses, texts = List.split entries in
+ statuses, texts
+ in
+ history <- new_statuses @ history;
+ statements <- new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let new_text = String.concat "" (List.rev new_statements) in
+ if statement <> None then
+ buffer#insert ~iter:start new_text
+ else begin
+ if new_text <> String.sub s 0 parsed_len then begin
+ buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
+ buffer#insert ~iter:start new_text;
+ end;
+ end;
+ self#moveMark (String.length new_text);
+ (* here we need to set the Goal in case we are going to cursor (or to
+ 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 <- None
method private _retract offset lexicon_status grafite_status new_statements
new_history
method private reset_buffer =
statements <- [];
history <- [ initial_statuses ];
- userGoal <- ~-1;
+ userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
(* method proofStatus = MatitaTypes.get_proof_status self#status *)
method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status
+
method proofContext =
- GrafiteTypes.get_proof_context self#grafite_status userGoal
+ match userGoal with
+ None -> assert false
+ | Some n ->
+ GrafiteTypes.get_proof_context self#grafite_status n
+
method proofConclusion =
- GrafiteTypes.get_proof_conclusion self#grafite_status userGoal
+ match userGoal with
+ None -> assert false
+ | Some n ->
+ GrafiteTypes.get_proof_conclusion self#grafite_status n
+
method stack = GrafiteTypes.get_stack self#grafite_status
- method setGoal n = userGoal <- n
+ method setGoal n = userGoal <- Some n
method goal = userGoal
method eos =
projects / helm.git / blobdiff