| TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
| _ -> MatitaSync.alias_diff ~from:status new_status
in
- (* we remove the defined object since we consider them "automathic aliases" *)
+ (* we remove the defined object since we consider them "automatic aliases" *)
let new_aliases =
let module DTE = DisambiguateTypes.Environment in
let module UM = UriManager in
with
MatitaEngine.UnableToInclude what as exc ->
let compile_needed_and_go_on d =
- let root = MatitamakeLib.root_for_development d in
- let target = root ^ "/" ^ what in
+ let target = what in
let refresh_cb () =
while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
in
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _) ->
(try
- (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
| None -> ()
| Some u ->
- if not (ML.is_empty u) then
+ if not (MatitaMisc.is_empty u) then
match
guistuff.ask_confirmation
~title:"Baseuri redefinition"
| TA.Macro (_,mac) ->
eval_macro guistuff status parsed_text script mac
-let rec eval_statement guistuff status user_goal script s =
+let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
+ guistuff status user_goal script s
+=
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let st = GrafiteParser.parse_statement (Stream.of_string s) in
+ let st =
+ try
+ GrafiteParser.parse_statement (Stream.of_string s)
+ with
+ CicNotationParser.Parse_error (floc,err) as exc ->
+ let (x, y) = CicNotationPt.loc_of_floc floc in
+ let x = parsedlen + x in
+ let y = parsedlen + y in
+ let x' = baseoffset + x in
+ let y' = baseoffset + y in
+ let x_iter = buffer#get_iter (`OFFSET x') in
+ let y_iter = buffer#get_iter (`OFFSET y') in
+ buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+ let id = ref None in
+ id :=
+ Some
+ (buffer#connect#changed
+ ~callback:(
+ fun () ->
+ buffer#remove_tag error_tag ~start:buffer#start_iter
+ ~stop:buffer#end_iter;
+ match !id with
+ None -> assert false (* a race condition occurred *)
+ | Some id ->
+ (new GObj.gobject_ops buffer#as_buffer)#disconnect id));
+ let flocb,floce = floc in
+ let floc =
+ {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y } in
+ raise (CicNotationParser.Parse_error (floc,err))
+ in
let text_of_loc loc =
let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
let parsed_text = safe_substring s 0 parsed_text_length in
let remain_len = String.length s - parsed_text_length in
let s = String.sub s parsed_text_length remain_len in
let s,len =
- eval_statement guistuff status user_goal script s
+ eval_statement baseoffset (parsedlen + parsed_text_length) error_tag
+ buffer guistuff status user_goal script s
in
(match s with
| (status, text) :: tl ->
val locked_mark =
buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
+ val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
method locked_mark = locked_mark
+ method locked_tag = locked_tag
(* history can't be empty, the invariant above grant that it contains at
* least the init status *)
let s = match statement with Some s -> s | None -> self#getFuture in
MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
let (entries, parsed_len) =
- eval_statement guistuff self#status userGoal self s
+ eval_statement (buffer#get_iter_at_mark (`MARK locked_mark))#offset 0
+ error_tag buffer guistuff self#status userGoal self s
in
let (new_statuses, new_statements) = List.split entries in
-(*
-prerr_endline "evalStatement returned";
-List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
-*)
history <- List.rev new_statuses @ history;
statements <- List.rev new_statements @ statements;
let start = buffer#get_iter_at_mark (`MARK locked_mark) in
let new_text = String.concat "" new_statements in
- if new_text <> String.sub s 0 parsed_len then
+ if statement <> None then
+ buffer#insert ~iter:start new_text
+ else
+ if new_text <> String.sub s 0 parsed_len then
begin
-(* prerr_endline ("new:" ^ new_text); *)
-(* prerr_endline ("s:" ^ String.sub s 0 parsed_len); *)
- let stop = start#copy#forward_chars parsed_len in
- buffer#delete ~start ~stop;
- buffer#insert ~iter:start new_text;
-(* prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *)
+ let stop = start#copy#forward_chars parsed_len in
+ buffer#delete ~start ~stop;
+ buffer#insert ~iter:start new_text;
end;
self#moveMark (String.length new_text)
let status = self#status in
List.iter (fun o -> o status) observers
- method loadFromFile () =
- buffer#set_text (MatitaMisc.input_file self#getFilename);
+ method loadFromFile f =
+ buffer#set_text (MatitaMisc.input_file f);
self#goto_top;
buffer#set_modified false
projects / helm.git / blobdiff