| 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
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 *)
~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
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 *)