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' =
() =
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