| None -> []
| Some devel -> [MatitamakeLib.root_for_development devel ]
in
+ let include_ =
+ include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+ 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
(* | Incomplete_proof { stack = stack }
when not (List.mem user_goal (Continuationals.head_goals stack)) ->
let status =
- MatitaEngine.eval_ast ~include_paths:include_
+ MatitaEngine.eval_ast
~do_heavy_checks:true status (goal_ast user_goal)
in
let initial_space = if initial_space = "" then "\n" else initial_space
| _ -> initial_space,status,[] in
let new_status =
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ~include_paths:include_ ~do_heavy_checks:true new_status st
+ ~do_heavy_checks:true new_status st
in
let new_aliases =
match ex with
try
eval_with_engine guistuff status user_goal parsed_text st
with
- | GrafiteEngine.UnableToInclude what
+ | GrafiteParserMisc.UnableToInclude what
| GrafiteEngine.IncludedFileNotCompiled what as exc ->
let compile_needed_and_go_on d =
let target = what in
match interps with
| [_,_,x,_], _ -> x
| _ -> assert false
+
+let pp_eager_statement_ast =
+ GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
let module TAPp = GrafiteAstPp in
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
+ (* XXX use a real CIC -> string pretty printer *)
+ let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
| TA.WInstance (loc, term) ->
let term = disambiguate_macro_term term status user_goal in
let l = Whelp.instance ~dbd term in
- let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+ let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WLocate (loc, s) ->
let l = Whelp.locate ~dbd s in
- let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+ let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WElim (loc, term) ->
| _ -> failwith "Not a MutInd"
in
let l = Whelp.elim ~dbd uri in
- let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
+ let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WHint (loc, term) ->
let term = disambiguate_macro_term term status user_goal in
let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
- let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
+ let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
(* REAL macro *)
in
let new_status =
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(fun _ -> assert false)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
status ast in
let extra_text =
- comment parsed_text ^
- "\n" ^ TAPp.pp_statement ast
- in
+ comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
[ new_status , (extra_text, ast) ], parsed_text_length
| _ ->
HLog.error
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
(try
- (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
| None -> ()
| Some u ->
if not (GrafiteMisc.is_empty u) then
LibraryClean.clean_baseuris ~basedir [u]
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- eval_with_engine
- guistuff status user_goal parsed_text (TA.Executable (loc, ex))
+ eval_with_engine
+ guistuff status user_goal parsed_text (TA.Executable (loc, ex))
with MatitaTypes.Cancel -> [], 0)
| TA.Macro (_,mac) ->
eval_macro guistuff status user_goal unparsed_text parsed_text script mac
fun () -> incr i; !i
class script ~(source_view: GSourceView.source_view)
- ~(init: GrafiteTypes.status)
~(mathviewer: MatitaTypes.mathViewer)
~set_star
~ask_confirmation
(fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
val mutable statements = []; (** executed statements *)
- val mutable history = [ init ];
+ val mutable history = [ MatitaSync.init () ];
(** list of states before having executed statements. Head element of this
* list is the current state, last element is the state at the beginning of
* the script.
let start = buffer#get_iter_at_mark (`MARK locked_mark) in
let new_text = String.concat "" new_statements in
if statement <> None then
- buffer#insert ~iter:start new_text
- else
+ 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
- let stop = start#copy#forward_chars parsed_len in
- buffer#delete ~start ~stop;
+ 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);
(*
(match List.rev new_asts with (* advance again on punctuation *)
end
method private goto_top =
+ let init =
+ let rec last x = function
+ | [] -> x
+ | hd::tl -> last hd tl
+ in
+ last self#status history
+ in
+ (* FIXME: this is not correct since there is no undo for
+ * library_objects.set_default... *)
MatitaSync.time_travel ~present:self#status ~past:init
method private reset_buffer =
statements <- [];
- history <- [ init ];
+ history <- [ MatitaSync.init () ];
userGoal <- ~-1;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
source_buffer#begin_not_undoable_action ();
buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
source_buffer#end_not_undoable_action ();
- buffer#set_modified false
+ buffer#set_modified false;
method template () =
let template = HExtlib.input_file BuildTimeConf.script_template in
let _script = ref None
-let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
=
let s = new script
- ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star ()
+ ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star ()
in
_script := Some s;
s
projects / helm.git / blobdiff