From db88f09dfd6da59000c93e2ea1ea8565ec8e101d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Jul 2005 16:01:19 +0000 Subject: [PATCH] Highlighting of parse errors implemented. --- helm/matita/matita.txt | 5 ++-- helm/matita/matitaGui.ml | 23 +++++++++-------- helm/matita/matitaScript.ml | 49 ++++++++++++++++++++++++++++--------- 3 files changed, 53 insertions(+), 24 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 68b73f36c..9026e63b3 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -46,10 +46,8 @@ TODO GUI GRAFICA + - cut&paste stile "X": rimane la parte blu e lockata! - integrare il famoso logo mancante (anche nell'About dialog) - - highlight degli errori di parsing nello script (usando lo sfondo come per la - parte lockata di testo, da ripulire quando si modifica il testo o si sposta - il punto di esecuzione) - invertibilita' dell'inserimento automatico di alias: quando si torna su bisognerebbe tornare su di un passo e non fare undo degli alias (Zack: nella history ci sono anche gli offset per sapere a che pezzo di @@ -78,6 +76,7 @@ TODO - non chiudere transitivamente i moo ?? DONE +- highlight degli errori di parsing nello script -> CSC - quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo dalla finestra principale!!! -> CSC - sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 066d07cc5..733d0aab9 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -374,8 +374,13 @@ class gui () = let locker f = fun () -> lock_world (); - try f ();unlock_world () with exc -> unlock_world (); raise exc - in + try f ();unlock_world () with exc -> unlock_world (); raise exc in + let keep_focus f = + fun () -> + try + f (); source_view#misc#grab_focus () + with + exc -> source_view#misc#grab_focus (); raise exc in (* developments win *) let model = new MatitaGtkMisc.multiStringListModel @@ -631,19 +636,17 @@ class gui () = in let cursor () = source_buffer#place_cursor - (source_buffer#get_iter_at_mark (`NAME "locked")); - source_view#misc#grab_focus () - in + (source_buffer#get_iter_at_mark (`NAME "locked")) in let advance _ = (MatitaScript.instance ())#advance (); cursor () in let retract _ = (MatitaScript.instance ())#retract (); cursor () in let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in - let advance = locker advance in - let retract = locker retract in - let top = locker top in - let bottom = locker bottom in - let jump = locker jump in + let advance = locker (keep_focus advance) in + let retract = locker (keep_focus retract) in + let top = locker (keep_focus top) in + let bottom = locker (keep_focus bottom) in + let jump = locker (keep_focus jump) in let connect_key sym f = connect_key self#main#mainWinEventBox#event ~modifiers:[`CONTROL] ~stop:true sym f; diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4d092ca65..811b1a858 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -354,9 +354,40 @@ let eval_executable guistuff status user_goal parsed_text script ex = | 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 @@ -368,7 +399,8 @@ let rec eval_statement guistuff status user_goal script s = 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 -> @@ -432,6 +464,7 @@ object (self) 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 @@ -443,13 +476,10 @@ object (self) 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 @@ -459,12 +489,9 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; 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!!!!!" *) end; self#moveMark (String.length new_text) -- 2.39.2