(** raised when one of the script margins (top or bottom) is reached *)
exception Margin
exception NoUnfinishedProof
-exception ActionCancelled
+exception ActionCancelled of string
let safe_substring s i j =
try String.sub s i j with Invalid_argument _ -> assert false
else
f arg
in
- let do_nothing () = raise ActionCancelled in
+ let do_nothing () = raise (ActionCancelled "Inclusion not performed") in
let handle_with_devel d =
let name = MatitamakeLib.name_for_development d in
let title = "Unable to include " ^ what 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
+ let pp_macro =
+ let f t = ProofEngineReduction.replace
+ ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false)
+ ~what:[()] ~with_what:[Cic.Implicit None] ~where:t
+ in
+ let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+ TAPp.pp_macro
+ ~term_pp:(fun x ->
+ ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x))
+ in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
let l = Whelp.match_term ~dbd term in
- let query_url =
- MatitaMisc.strip_suffix ~suffix:"."
- (HExtlib.trim_blanks unparsed_text)
- in
- let entry = `Whelp (query_url, l) in
+ let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WInstance (loc, term) ->
let l = Whelp.instance ~dbd term in
- let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
+ let entry = `Whelp (pp_macro mac, 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 (pp_macro (TA.WLocate (loc, s)), l) in
+ let entry = `Whelp (pp_macro mac, 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 (pp_macro (TA.WElim (loc, term)), l) in
+ let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WHint (loc, term) ->
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 (pp_macro (TA.WHint (loc, term)), l) in
+ let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
(* REAL macro *)
begin
match ex with
| TA.Command (_,TA.Set (_,"baseuri",u)) ->
- if not (GrafiteMisc.is_empty u) then
+ if Http_getter_storage.is_read_only u then
+ raise (ActionCancelled ("baseuri " ^ u ^ " is readonly"));
+ if not (Http_getter_storage.is_empty u) then
(match
guistuff.ask_confirmation
~title:"Baseuri redefinition"
"Do you want to redefine the corresponding "^
"part of the library?")
with
- | `YES ->
- let basedir = Helm_registry.get "matita.basedir" in
- LibraryClean.clean_baseuris ~basedir [u]
+ | `YES -> LibraryClean.clean_baseuris [u]
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel)
| _ -> ()
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
-let initial_statuses =
+let initial_statuses () =
(* these include_paths are used only to load the initial notation *)
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
val mutable statements = [] (** executed statements *)
- val mutable history = [ initial_statuses ]
+ val mutable history = [ initial_statuses () ]
(** 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.
self#notify
with
| Margin -> self#notify
+ | Not_found -> assert false
| exc -> self#notify; raise exc
method retract () =
method private reset_buffer =
statements <- [];
- history <- [ initial_statuses ];
+ history <- [ initial_statuses () ];
userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
try
is_there_only_comments self#lexicon_status s
with
+ | HExtlib.Localized _
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true