From 5ee4e9d9fbff19b7937459c5ad4652542ac1ccb8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 3 Dec 2004 16:30:13 +0000 Subject: [PATCH] snapshot --- helm/matita/Makefile.in | 2 +- helm/matita/matita.glade | 12 +++++------ helm/matita/matita.ml | 1 + helm/matita/matitaConsole.ml | 32 +++++++++++++++++++++++------- helm/matita/matitaGeneratedGui.ml | 30 ++++++++++++++-------------- helm/matita/matitaGeneratedGui.mli | 20 +++++++++---------- helm/matita/matitaGui.ml | 6 ++++-- helm/matita/matitaMathView.ml | 9 ++++----- helm/matita/matitaMisc.ml | 4 ++++ helm/matita/matitaMisc.mli | 2 ++ 10 files changed, 72 insertions(+), 46 deletions(-) diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index e7f4f677b..a9ea5d40c 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -7,7 +7,7 @@ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O) OCAML_THREADS_FLAGS = -thread -OCAML_DEBUG_FLAGS = +OCAML_DEBUG_FLAGS = -g OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 6420b2aa5..103e27673 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -94,7 +94,7 @@ - + True gtk-open 1 @@ -115,7 +115,7 @@ - + True gtk-save 1 @@ -135,7 +135,7 @@ True - + True gtk-save-as 1 @@ -162,7 +162,7 @@ - + True gtk-quit 1 @@ -246,7 +246,7 @@ True Toggle console True - + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 7c9502bd4..49488a94d 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -232,6 +232,7 @@ let _ = (** *) let _ = +(* CicEnvironment.set_trust (fun _ -> false); *) (try load_script Sys.argv.(1) with Invalid_argument _ -> ()); diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 222055e65..889d8e2d8 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -31,6 +31,7 @@ open MatitaTypes let default_prompt = "" let default_phrase_sep = "." let default_callback = fun (phrase: string) -> true +let bullet = "∙" let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] @@ -92,6 +93,7 @@ class console val history = new history BuildTimeConf.console_history_size val mutable handle_position = 450 + val mutable last_phrase = "" initializer let buf = self#buffer in @@ -107,13 +109,15 @@ class console (Pcre.pmatch ~rex:trailing_NL_RE text) then let inserted_text = - buf#get_text - ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) - ~stop:buf#end_iter () + MatitaMisc.strip_trailing_blanks + (buf#get_text + ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) + ~stop:buf#end_iter ()) in let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *) self#lock; + last_phrase <- inserted_text; self#invoke_callback inserted_text; self#echo_prompt () end)); @@ -141,15 +145,13 @@ class console buf#insert ~iter:buf#end_iter phrase method private invoke_callback phrase = - history#add (* do not push trailing phrase separator *) - (String.sub phrase 0 - (String.length phrase - String.length _phrase_sep)); + history#add phrase; if _callback phrase then begin self#hide (); self#clear () + end (* else callback encountered troubles, don't hide console which probably contains error message *) - end method clear () = let buf = self#buffer in @@ -221,6 +223,21 @@ class console | StatefulProofEngine.Tactic_failure exn -> self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn)); false + | CicTextualParser2.Parse_error (floc, msg) -> + let buf = self#buffer in + let (x, y) = CicAst.loc_of_floc floc in + let red = buf#create_tag [`FOREGROUND "red"] in + let (start_error_pos, end_error_pos) = + buf#end_iter#backward_chars (String.length last_phrase - x), + buf#end_iter#backward_chars (String.length last_phrase - y) + in + if x - y = 0 then (* no region to highlight, let's add an hint about + where the error occured *) + buf#insert ~iter:end_error_pos ~tags:[red] bullet + else (* highlight the region where the error occured *) + buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos; + self#echo_error (sprintf "at character %d-%d: %s" x y msg); + false | exn -> self#echo_error (sprintf "Uncaught exception: %s" (Printexc.to_string exn)); @@ -241,3 +258,4 @@ let console in new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view +(* vim: set encoding=utf8: *) diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 883cb634e..f21a1967b 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -36,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata)) method newMenu = newMenu - val image174 = + val image182 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image174" ~info:"GtkImage" xmldata)) - method image174 = image174 + (Glade.get_widget_msg ~name:"image182" ~info:"GtkImage" xmldata)) + method image182 = image182 val newMenu_menu = new GMenu.menu (GtkMenu.Menu.cast (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) @@ -56,26 +56,26 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata)) method openMenuItem = openMenuItem - val image175 = + val image183 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image175" ~info:"GtkImage" xmldata)) - method image175 = image175 + (Glade.get_widget_msg ~name:"image183" ~info:"GtkImage" xmldata)) + method image183 = image183 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image176 = + val image184 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image176" ~info:"GtkImage" xmldata)) - method image176 = image176 + (Glade.get_widget_msg ~name:"image184" ~info:"GtkImage" xmldata)) + method image184 = image184 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image177 = + val image185 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image177" ~info:"GtkImage" xmldata)) - method image177 = image177 + (Glade.get_widget_msg ~name:"image185" ~info:"GtkImage" xmldata)) + method image185 = image185 val separator1 = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) @@ -84,10 +84,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) method quitMenuItem = quitMenuItem - val image178 = + val image186 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image178" ~info:"GtkImage" xmldata)) - method image178 = image178 + (Glade.get_widget_msg ~name:"image186" ~info:"GtkImage" xmldata)) + method image186 = image186 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 74b2adfd0..6572f1a6d 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -16,11 +16,11 @@ class mainWin : val helpMenu_menu : GMenu.menu val hideConsoleButton : GButton.button val image169 : GMisc.image - val image174 : GMisc.image - val image175 : GMisc.image - val image176 : GMisc.image - val image177 : GMisc.image - val image178 : GMisc.image + val image182 : GMisc.image + val image183 : GMisc.image + val image184 : GMisc.image + val image185 : GMisc.image + val image186 : GMisc.image val mainMenuBar : GMenu.menu_shell val mainStatusBar : GMisc.statusbar val mainVPanes : GPack.paned @@ -64,11 +64,11 @@ class mainWin : method helpMenu_menu : GMenu.menu method hideConsoleButton : GButton.button method image169 : GMisc.image - method image174 : GMisc.image - method image175 : GMisc.image - method image176 : GMisc.image - method image177 : GMisc.image - method image178 : GMisc.image + method image182 : GMisc.image + method image183 : GMisc.image + method image184 : GMisc.image + method image185 : GMisc.image + method image186 : GMisc.image method mainMenuBar : GMenu.menu_shell method mainStatusBar : GMisc.statusbar method mainVPanes : GPack.paned diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 26cf9df08..6687ca69d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -81,8 +81,9 @@ class gui file = List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]); - (* "global" key bindings *) - List.iter (fun (key, callback) -> self#addKeyBinding key callback) + (* key bindings *) + List.iter (* global key bindings *) + (fun (key, callback) -> self#addKeyBinding key callback) [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, @@ -91,6 +92,7 @@ class gui file = toggle_win ~check:main#showScriptMenuItem script#scriptWin; GdkKeysyms._x, (fun () -> console#toggle ()); ]; + add_key_binding GdkKeysyms._Escape console#hide main#consoleEventBox; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); ignore (main#aboutMenuItem#connect#activate (fun _ -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index bb62f51c9..8c38cfc0b 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -91,8 +91,8 @@ class proof_viewer obj = ApplyTransformation.mml_of_cic_object ~explode_all:true (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types in - debug_print "load_proof: dumping MathML to /tmp/proof"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ()); + debug_print "load_proof: dumping MathML to ./proof"; + ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ()); match current_mathml with | None -> self#load_root ~root:mathml#get_documentElement ; @@ -165,8 +165,8 @@ class sequent_viewer obj = ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); - debug_print "load_sequent: dumping MathML to /tmp/prova"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ()); + debug_print "load_sequent: dumping MathML to ./prova"; + ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement end @@ -237,7 +237,6 @@ class sequents_viewer ~(notebook:GPack.notebook) sequent_viewer#load_sequent _metasenv goal; try List.assoc goal goal2win (); - debug_print "set_selection none"; sequent_viewer#set_selection None with Not_found -> assert false diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 83bdeb36f..1a55795a5 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -45,3 +45,7 @@ let append_phrase_sep s = else s +let strip_trailing_blanks = + let rex = Pcre.regexp "\\s*$" in + fun s -> Pcre.replace ~rex s + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index f8e8ee40c..7a9ac0fc6 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -38,3 +38,5 @@ val is_proof_object: string -> bool * it *) val append_phrase_sep: string -> string +val strip_trailing_blanks: string -> string + -- 2.39.2