From bb42469b8aa1ccb0b2a5ca1d402c43ed0def1c08 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 31 Oct 2006 12:33:21 +0000 Subject: [PATCH] The OK button of the disambiguation errors interface now adds aliases to the current script. However, the aliases are used only in passes 1 and 3 :-( --- helm/software/matita/matitaGui.ml | 87 +++++++++++++++++++--------- helm/software/matita/matitaScript.ml | 6 ++ 2 files changed, 65 insertions(+), 28 deletions(-) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index c718bd81a..ff00ce27b 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -232,8 +232,7 @@ class interpErrorModel = end -let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn - offset errorll +let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll = let errorll' = if all_passes then errorll else @@ -314,37 +313,69 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn dialog#disambiguationErrors#set_title "Disambiguation error"; dialog#disambiguationErrorsLabel#set_label "Click on an error to see the corresponding message:"; - ignore (dialog#treeview#connect#cursor_changed (fun _ -> - let tree_path = - match fst (dialog#treeview#get_cursor ()) with - None -> assert false - | Some tp -> tp in - let idx1,idx2,idx3 = model#get_interp_no tree_path in - let loffset,lll = List.nth choices idx1 in - let _,envs_and_diffs,msg = - match idx2 with - Some idx2 -> List.nth lll idx2 - | None -> [],[],lazy "Multiple error messages. Please select one." in - let _,env,diff = - match idx3 with - Some idx3 -> List.nth envs_and_diffs idx3 - | None -> [],[],[] (* dymmy value, used *) in - let script = MatitaScript.current () in - let error_tag = script#error_tag in - source_buffer#remove_tag error_tag - ~start:source_buffer#start_iter - ~stop:source_buffer#end_iter; - notify_exn - (GrafiteDisambiguator.DisambiguationError - (offset,[[env,diff,loffset,msg]])) - )); + ignore (dialog#treeview#connect#cursor_changed + (fun _ -> + let tree_path = + match fst (dialog#treeview#get_cursor ()) with + None -> assert false + | Some tp -> tp in + let idx1,idx2,idx3 = model#get_interp_no tree_path in + let loffset,lll = List.nth choices idx1 in + let _,envs_and_diffs,msg = + match idx2 with + Some idx2 -> List.nth lll idx2 + | None -> [],[],lazy "Multiple error messages. Please select one." in + let _,env,diff = + match idx3 with + Some idx3 -> List.nth envs_and_diffs idx3 + | None -> [],[],[] (* dymmy value, used *) in + let script = MatitaScript.current () in + let error_tag = script#error_tag in + source_buffer#remove_tag error_tag + ~start:source_buffer#start_iter + ~stop:source_buffer#end_iter; + notify_exn + (GrafiteDisambiguator.DisambiguationError + (offset,[[env,diff,loffset,msg]])) + )); let return _ = dialog#disambiguationErrors#destroy (); GMain.Main.quit () in let fail _ = return () in - ignore (dialog#disambiguationErrors#event#connect#delete (fun _ -> true)); - connect_button dialog#disambiguationErrorsOkButton (fun _ -> return ()); + ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true)); + connect_button dialog#disambiguationErrorsOkButton + (fun _ -> + let tree_path = + match fst (dialog#treeview#get_cursor ()) with + None -> assert false + | Some tp -> tp in + let idx1,idx2,idx3 = model#get_interp_no tree_path in + let diff = + match idx2,idx3 with + Some idx2, Some idx3 -> + let _,lll = List.nth choices idx1 in + let _,envs_and_diffs,_ = List.nth lll idx2 in + let _,_,diff = List.nth envs_and_diffs idx3 in + diff + | _,_ -> assert false + in + let newtxt = + String.concat "\n" + ("" :: + List.map + (fun k,value -> + DisambiguatePp.pp_environment + (DisambiguateTypes.Environment.add k value + DisambiguateTypes.Environment.empty)) + diff) ^ "\n" + in + source_buffer#insert + ~iter: + (source_buffer#get_iter_at_mark + (`NAME "beginning_of_statement")) newtxt ; + return () + ); connect_button dialog#disambiguationErrorsMoreErrors (fun _ -> return () ; interactive_error_interp ~all_passes:true source_buffer notify_exn offset diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 23de391c6..0e5121309 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -363,6 +363,9 @@ script ex loc | `CANCEL -> raise MatitaTypes.Cancel) | _ -> () end; + ignore (buffer#move_mark (`NAME "beginning_of_statement") + ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars + (Glib.Utf8.length skipped_txt))) ; eval_with_engine guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) @@ -501,6 +504,9 @@ object (self) (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter + val beginning_of_statement_mark = + buffer#create_mark ~name:"beginning_of_statement" + ~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"] -- 2.39.2