(** 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
let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
-let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)((.|\n)*)"
+let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)"
let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
let multiline_RE = Pcre.regexp "^\n[^\n]+$"
let newline_RE = Pcre.regexp "\n"
let initial_space,parsed_text =
try
let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
- pieces.(1), pieces.(2)
+ let p1 = pieces.(1) in
+ let p1_len = String.length p1 in
+ let rest = String.sub parsed_text p1_len (parsed_text_length - p1_len) in
+ p1, rest
with
Not_found -> "", parsed_text in
let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
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
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.
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