From: Stefano Zacchiroli Date: Wed, 27 Oct 2004 11:50:26 +0000 (+0000) Subject: snapshot, notably: X-Git-Tag: V_0_0_10~5 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d431843f49b3658593c8cc918b53a43479a6486;p=helm.git snapshot, notably: - ported to Dbi disambiguation - started implementation of coqide-like script window --- diff --git a/helm/matita/.depend b/helm/matita/.depend index d348338e8..4aadffba2 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -9,21 +9,23 @@ matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmo matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ - matitaGtkMisc.cmi matitaGui.cmi + matitaGtkMisc.cmi matitaMisc.cmi matitaGui.cmi matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ - matitaGtkMisc.cmx matitaGui.cmi + matitaGtkMisc.cmx matitaMisc.cmx matitaGui.cmi matitaInterpreter.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGui.cmi \ matitaMathView.cmi matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi matitaInterpreter.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGui.cmx \ matitaMathView.cmx matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi matitaMathView.cmo: matitaCicMisc.cmo matitaTypes.cmo matitaMathView.cmi matitaMathView.cmx: matitaCicMisc.cmx matitaTypes.cmx matitaMathView.cmi +matitaMisc.cmo: matitaMisc.cmi +matitaMisc.cmx: matitaMisc.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ - matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaProof.cmi \ - matitaTypes.cmo + matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaMisc.cmi \ + matitaProof.cmi matitaTypes.cmo matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ - matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaProof.cmx \ - matitaTypes.cmx + matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaMisc.cmx \ + matitaProof.cmx matitaTypes.cmx matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmo matitaTypes.cmo \ matitaProof.cmi matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \ diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index eba88af12..7b3805751 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -8,11 +8,13 @@ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O) OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -OCAMLC = $(OCAMLFIND) ocamlc $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) +OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) CMOS = \ buildTimeConf.cmo \ + matitaMisc.cmo \ matitaGeneratedGui.cmo \ matitaTypes.cmo \ matitaCicMisc.cmo \ diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 249058f8b..bb3391317 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -29,4 +29,5 @@ let undo_history_size = 10;; let console_history_size = 100;; let gtkrc = "@MATITA_GTKRC@";; let base_uri = "cic:/matita";; +module DB = @DBI_MODULE@;; diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index c83b4af0e..2cf2e52b8 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -27,10 +27,14 @@ else AC_MSG_ERROR(could not find camlp4o) fi +DBI_DRIVER="mysql" + FINDLIB_REQUIRES="\ lablgtk2.glade \ lablgtkmathview \ pcre \ +dbi.$DBI_DRIVER \ +unix \ helm-cic_omdoc \ helm-cic_transformations \ helm-registry \ @@ -83,6 +87,7 @@ if test "$DEBUG" = "true"; then fi MATITA_GTKRC="matita.gtkrc" +DBI_MODULE="Dbi_$DBI_DRIVER" AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) @@ -92,6 +97,7 @@ AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) AC_SUBST(MATITA_GTKRC) +AC_SUBST(DBI_MODULE) AC_OUTPUT([ buildTimeConf.ml diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 7df0d1961..389a14e8d 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -4,32 +4,15 @@ matita.glade true -
- mathql_db_map.txt -
- mowgli.cs.unibo.it - - mowgli - - - helm -
- dbname=mowgli host=mowgli.cs.unibo.it user=helm - - - - - - - - - - - +
+ + localhost + helm + mowgli
remote - http://mowgli.cs.unibo.it:58081/ - + + http://localhost:58081/
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 466174ba3..e7dc8ded4 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -93,7 +93,7 @@ - + True gtk-open 1 @@ -114,7 +114,7 @@ - + True gtk-save 1 @@ -134,7 +134,7 @@ True - + True gtk-save-as 1 @@ -161,7 +161,7 @@ - + True gtk-quit 1 @@ -223,6 +223,16 @@ + + + + True + Show Script Window + True + False + + + @@ -418,7 +428,7 @@ True - + True True True @@ -428,7 +438,7 @@ - + True True True @@ -999,7 +1009,7 @@ Copyright (C) 2004, 0 True - * + * False @@ -1266,4 +1276,192 @@ Copyright (C) 2004, + + Matita: script + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + 300 + 800 + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + True + False + + + + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + go back 1 phrase + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + execute til cursor + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + go forward 1 phrase + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + 0 + False + False + + + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + 0 + True + True + + + + + + + + diff --git a/helm/matita/matita.gtkrc b/helm/matita/matita.gtkrc new file mode 100644 index 000000000..91081c311 --- /dev/null +++ b/helm/matita/matita.gtkrc @@ -0,0 +1,80 @@ +# Based on /usr/share/themes/Emacs/gtk-2.0-key/, +# modified by Zack for matita + +# +# A keybinding set implementing emacs-like keybindings +# + +# +# Bindings for GtkTextView and GtkEntry +# +binding "gtk-emacs-text-entry" +{ + bind "b" { "move-cursor" (logical-positions, -1, 0) } + bind "b" { "move-cursor" (logical-positions, -1, 1) } + bind "f" { "move-cursor" (logical-positions, 1, 0) } + bind "f" { "move-cursor" (logical-positions, 1, 1) } + + bind "b" { "move-cursor" (words, -1, 0) } + bind "b" { "move-cursor" (words, -1, 1) } + bind "f" { "move-cursor" (words, 1, 0) } + bind "f" { "move-cursor" (words, 1, 1) } + + bind "a" { "move-cursor" (paragraph-ends, -1, 0) } + bind "a" { "move-cursor" (paragraph-ends, -1, 1) } + bind "e" { "move-cursor" (paragraph-ends, 1, 0) } + bind "e" { "move-cursor" (paragraph-ends, 1, 1) } + + bind "w" { "cut-clipboard" () } + bind "y" { "paste-clipboard" () } + + bind "d" { "delete-from-cursor" (chars, 1) } + bind "d" { "delete-from-cursor" (word-ends, 1) } + bind "k" { "delete-from-cursor" (paragraph-ends, 1) } + bind "backslash" { "delete-from-cursor" (whitespace, 1) } + + bind "space" { "delete-from-cursor" (whitespace, 1) + "insert-at-cursor" (" ") } + bind "KP_Space" { "delete-from-cursor" (whitespace, 1) + "insert-at-cursor" (" ") } + + # + # Some non-Emacs keybindings people are attached to + # + bind "u" { + "move-cursor" (paragraph-ends, -1, 0) + "delete-from-cursor" (paragraph-ends, 1) + } + bind "h" { "delete-from-cursor" (chars, -1) } + bind "w" { "delete-from-cursor" (word-ends, -1) } +} + +# +# Bindings for GtkTextView +# +binding "gtk-emacs-text-view" +{ +# bind "p" { "move-cursor" (display-lines, -1, 0) } + bind "p" { "move-cursor" (display-lines, -1, 1) } +# bind "n" { "move-cursor" (display-lines, 1, 0) } + bind "n" { "move-cursor" (display-lines, 1, 1) } + + bind "space" { "set-anchor" () } + bind "KP_Space" { "set-anchor" () } +} + +# +# Bindings for GtkTreeView +# +binding "gtk-emacs-tree-view" +{ + bind "s" { "start-interactive-search" () } + bind "f" { "move-cursor" (logical-positions, 1) } + bind "b" { "move-cursor" (logical-positions, -1) } +} + +class "GtkEntry" binding "gtk-emacs-text-entry" +class "GtkTextView" binding "gtk-emacs-text-entry" +class "GtkTextView" binding "gtk-emacs-text-view" +class "GtkTreeView" binding "gtk-emacs-tree-view" + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index fb163aa9c..b946ec69b 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -26,6 +26,10 @@ open Printf open MatitaGtkMisc +open MatitaTypes +open MatitaMisc + +module DB = BuildTimeConf.DB (** {2 Internal status} *) @@ -40,28 +44,19 @@ let (get_proof, set_proof, has_proof) = (fun () -> (* has_proof *) !current_proof <> None)) -(** {2 Settings} *) - -let debug_print = MatitaTypes.debug_print - -let save_dom = - let domImpl = lazy (Gdome.domImplementation ()) in - fun ~doc ~dest -> - ignore - ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ()) - (** {2 Initialization} *) let _ = + Helm_registry.load_from "matita.conf.xml"; GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; - GtkMain.Main.init () -let _ = Helm_registry.load_from "matita.conf.xml" -let _ = GMain.Main.init () + GMain.Main.init () let parserr = new MatitaDisambiguator.parserr () -let mqiconn = MQIConn.init () +let dbh = + new DB.connection ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database") let gui = MatitaGui.instance () let disambiguator = - new MatitaDisambiguator.disambiguator ~parserr ~mqiconn + new MatitaDisambiguator.disambiguator ~parserr ~dbh ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () @@ -148,9 +143,24 @@ let _ = disambiguator#disambiguateTerm (Stream.of_string input) in let proof = MatitaProof.proof ~typ:expr ~metasenv () in - new_proof proof)) + new_proof proof)); + ignore (gui#main#openMenuItem#connect#activate (fun _ -> + match gui#chooseFile () with + | None -> () + | Some f when is_proof_script f -> + gui#script#scriptTextView#buffer#set_text (input_file f) + | Some f -> + gui#console#echo_error (sprintf + "Don't know what to do with file: %s\nUnrecognized file format." f))) (** *) + +let save_dom = + let domImpl = lazy (Gdome.domImplementation ()) in + fun ~doc ~dest -> + ignore + ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ()) + let _ = if BuildTimeConf.debug then begin gui#main#debugMenu#misc#show (); @@ -181,6 +191,7 @@ let _ = addDebugItem "dump proof status to stdout" (fun _ -> print_endline ((get_proof ())#toString)); end + (** *) let _ = GtkThread.main () diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 5fb44adf4..603a480f4 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -165,7 +165,8 @@ class console buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] (msg ^ "\n"); self#ignore_insert_text_signal false; - self#lock + self#lock; + self#echo_prompt () (** navigation methods: history, cursor motion, ... *) diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index daf64884c..23de092bd 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -30,7 +30,7 @@ class parserr () = end class disambiguator - ~parserr ~mqiconn ~(chooseUris: MatitaTypes.choose_uris_callback) + ~parserr ~dbh ~(chooseUris: MatitaTypes.choose_uris_callback) ~(chooseInterp: MatitaTypes.choose_interp_callback) () = let disambiguate_term = @@ -70,7 +70,7 @@ class disambiguator | Some env -> (false, env) | None -> (true, _env) in - match disambiguate_term mqiconn context metasenv termAst ~aliases:env with + match disambiguate_term ~dbh context metasenv termAst ~aliases:env with | [ (env, metasenv, term) as x ] -> if save_state then self#setEnv env; x diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 8397e4dbf..9b432f845 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -27,7 +27,7 @@ class parserr: unit -> MatitaTypes.parserr class disambiguator: parserr:MatitaTypes.parserr -> (** parser *) - mqiconn:MQIConn.handle -> (** mathql database connection *) + dbh:Dbi.connection -> chooseUris:MatitaTypes.choose_uris_callback -> chooseInterp:MatitaTypes.choose_interp_callback -> unit -> diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 943f78ff8..cb7200391 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 image116 = + val image128 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image116" ~info:"GtkImage" xmldata)) - method image116 = image116 + (Glade.get_widget_msg ~name:"image128" ~info:"GtkImage" xmldata)) + method image128 = image128 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 image117 = + val image129 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image117" ~info:"GtkImage" xmldata)) - method image117 = image117 + (Glade.get_widget_msg ~name:"image129" ~info:"GtkImage" xmldata)) + method image129 = image129 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image118 = + val image130 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image118" ~info:"GtkImage" xmldata)) - method image118 = image118 + (Glade.get_widget_msg ~name:"image130" ~info:"GtkImage" xmldata)) + method image130 = image130 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image119 = + val image131 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image119" ~info:"GtkImage" xmldata)) - method image119 = image119 + (Glade.get_widget_msg ~name:"image131" ~info:"GtkImage" xmldata)) + method image131 = image131 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 image120 = + val image132 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image120" ~info:"GtkImage" xmldata)) - method image120 = image120 + (Glade.get_widget_msg ~name:"image132" ~info:"GtkImage" xmldata)) + method image132 = image132 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) @@ -112,6 +112,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (Glade.get_widget_msg ~name:"ShowCheckMenuItem" ~info:"GtkCheckMenuItem" xmldata)) method showCheckMenuItem = showCheckMenuItem + val showScriptMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast + (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata)) + method showScriptMenuItem = showScriptMenuItem val debugMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) @@ -206,14 +210,14 @@ class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GWindow.file_selection (GtkWindow.FileSelection.cast (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) method fileSelectionWin = fileSelectionWin - val cancel_button1 = + val fileSelCancelButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"cancel_button1" ~info:"GtkButton" xmldata)) - method cancel_button1 = cancel_button1 - val ok_button1 = + (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata)) + method fileSelCancelButton = fileSelCancelButton + val fileSelOkButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ok_button1" ~info:"GtkButton" xmldata)) - method ok_button1 = ok_button1 + (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata)) + method fileSelOkButton = fileSelOkButton method check_widgets () = () end class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = @@ -539,9 +543,73 @@ class checkWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end +class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"ScriptWin" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"ScriptWin" ~info:"GtkWindow" xmldata)) + method toplevel = toplevel + val scriptWin = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"ScriptWin" ~info:"GtkWindow" xmldata)) + method scriptWin = scriptWin + val scriptWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata)) + method scriptWinEventBox = scriptWinEventBox + val vbox4 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"vbox4" ~info:"GtkVBox" xmldata)) + method vbox4 = vbox4 + val toolbar1 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar1" ~info:"GtkToolbar" xmldata)) + method toolbar1 = toolbar1 + val button5 = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"button5" ~info:"GtkButton" xmldata)) + method button5 = button5 + val image133 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata)) + method image133 = image133 + val button6 = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"button6" ~info:"GtkButton" xmldata)) + method button6 = button6 + val image134 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image134" ~info:"GtkImage" xmldata)) + method image134 = image134 + val button7 = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"button7" ~info:"GtkButton" xmldata)) + method button7 = button7 + val image135 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata)) + method image135 = image135 + val scrolledScript = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"ScrolledScript" ~info:"GtkScrolledWindow" xmldata)) + method scrolledScript = scrolledScript + val scriptTextView = + new GText.view (GtkText.View.cast + (Glade.get_widget_msg ~name:"ScriptTextView" ~info:"GtkTextView" xmldata)) + method scriptTextView = scriptTextView + method reparent parent = + scriptWinEventBox#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end let check_all ?(show=false) () = ignore (GMain.Main.init ()); + let scriptWin = new scriptWin () in + if show then scriptWin#toplevel#show (); + scriptWin#check_widgets (); let checkWin = new checkWin () in if show then checkWin#toplevel#show (); checkWin#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index d67a27549..3c646b10c 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -13,11 +13,11 @@ class mainWin : val fileMenu_menu : GMenu.menu val helpMenu : GMenu.menu_item val helpMenu_menu : GMenu.menu - val image116 : GMisc.image - val image117 : GMisc.image - val image118 : GMisc.image - val image119 : GMisc.image - val image120 : GMisc.image + val image128 : GMisc.image + val image129 : GMisc.image + val image130 : GMisc.image + val image131 : GMisc.image + val image132 : GMisc.image val mainMenuBar : GMenu.menu_shell val mainStatusBar : GMisc.statusbar val mainVPanes : GPack.paned @@ -39,6 +39,7 @@ class mainWin : val sequentsNotebook : GPack.notebook val showCheckMenuItem : GMenu.check_menu_item val showProofMenuItem : GMenu.check_menu_item + val showScriptMenuItem : GMenu.check_menu_item val showToolBarMenuItem : GMenu.check_menu_item val toplevel : GWindow.window val viewMenu : GMenu.menu_item @@ -56,11 +57,11 @@ class mainWin : method fileMenu_menu : GMenu.menu method helpMenu : GMenu.menu_item method helpMenu_menu : GMenu.menu - method image116 : GMisc.image - method image117 : GMisc.image - method image118 : GMisc.image - method image119 : GMisc.image - method image120 : GMisc.image + method image128 : GMisc.image + method image129 : GMisc.image + method image130 : GMisc.image + method image131 : GMisc.image + method image132 : GMisc.image method mainMenuBar : GMenu.menu_shell method mainStatusBar : GMisc.statusbar method mainVPanes : GPack.paned @@ -83,6 +84,7 @@ class mainWin : method sequentsNotebook : GPack.notebook method showCheckMenuItem : GMenu.check_menu_item method showProofMenuItem : GMenu.check_menu_item + method showScriptMenuItem : GMenu.check_menu_item method showToolBarMenuItem : GMenu.check_menu_item method toplevel : GWindow.window method viewMenu : GMenu.menu_item @@ -116,16 +118,16 @@ class fileSelectionWin : ?autoconnect:bool -> unit -> object - val cancel_button1 : GButton.button + val fileSelCancelButton : GButton.button + val fileSelOkButton : GButton.button val fileSelectionWin : GWindow.file_selection - val ok_button1 : GButton.button val toplevel : GWindow.file_selection val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit - method cancel_button1 : GButton.button method check_widgets : unit -> unit + method fileSelCancelButton : GButton.button + method fileSelOkButton : GButton.button method fileSelectionWin : GWindow.file_selection - method ok_button1 : GButton.button method toplevel : GWindow.file_selection method xml : Glade.glade_xml Gtk.obj end @@ -343,4 +345,42 @@ class checkWin : method toplevel : GWindow.window method xml : Glade.glade_xml Gtk.obj end +class scriptWin : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val button5 : GButton.button + val button6 : GButton.button + val button7 : GButton.button + val image133 : GMisc.image + val image134 : GMisc.image + val image135 : GMisc.image + val scriptTextView : GText.view + val scriptWin : GWindow.window + val scriptWinEventBox : GBin.event_box + val scrolledScript : GBin.scrolled_window + val toolbar1 : GButton.toolbar + val toplevel : GWindow.window + val vbox4 : GPack.box + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method button5 : GButton.button + method button6 : GButton.button + method button7 : GButton.button + method check_widgets : unit -> unit + method image133 : GMisc.image + method image134 : GMisc.image + method image135 : GMisc.image + method reparent : GObj.widget -> unit + method scriptTextView : GText.view + method scriptWin : GWindow.window + method scriptWinEventBox : GBin.event_box + method scrolledScript : GBin.scrolled_window + method toolbar1 : GButton.toolbar + method toplevel : GWindow.window + method vbox4 : GPack.box + method xml : Glade.glade_xml Gtk.obj + end val check_all : ?show:bool -> unit -> unit diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 212e4e4d9..6b70a498f 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -45,6 +45,7 @@ open Printf open MatitaGeneratedGui open MatitaGtkMisc +open MatitaMisc class gui file = (* creation order _is_ relevant for windows placement *) @@ -54,30 +55,36 @@ class gui file = let fileSel = new fileSelectionWin ~file () in let proof = new proofWin ~file () in let check = new checkWin ~file () in + let script = new scriptWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox; - check#checkWinEventBox ] + check#checkWinEventBox; script#scriptWinEventBox ] in let console = - MatitaConsole.console ~evbox:main#consoleEventBox + MatitaConsole.console ~evbox:main#consoleEventBox ~phrase_sep:";;" ~packing:main#scrolledConsole#add () in object (self) + val mutable chosen_file = None + initializer (* glade's check widgets *) 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 about; c fileSel; c main; c proof; c toolbar; c check; c script ]); (* show/hide commands *) toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; toggle_visibility proof#proofWin main#showProofMenuItem; toggle_visibility check#checkWin main#showCheckMenuItem; + toggle_visibility script#scriptWin main#showScriptMenuItem; (* "global" key bindings *) List.iter (fun (key, callback) -> self#addKeyBinding key callback) [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, toggle_win ~check:main#showCheckMenuItem check#checkWin; + GdkKeysyms._F5, + toggle_win ~check:main#showScriptMenuItem script#scriptWin; ]; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); @@ -87,6 +94,21 @@ class gui file = about#aboutWin#misc#hide ())); about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@" ~templ:BuildTimeConf.version about#aboutLabel#label); + (* file selection win *) + ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); + ignore (fileSel#fileSelectionWin#connect#response (fun event -> + let return r = + chosen_file <- r; + fileSel#fileSelectionWin#misc#hide (); + GMain.Main.quit () + in + match event with + | `OK -> + let fname = fileSel#fileSelectionWin#filename in + if is_regular fname then return (Some fname) + | `CANCEL -> return None + | `HELP -> () + | `DELETE_EVENT -> return None)); (* menus *) List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem; main#saveAsMenuItem ]; @@ -103,6 +125,7 @@ class gui file = method fileSel = fileSel method main = main method proof = proof + method script = script method toolbar = toolbar method newUriDialog () = @@ -136,6 +159,11 @@ class gui file = method setPhraseCallback = console#set_callback + method chooseFile () = + fileSel#fileSelectionWin#show (); + GtkThread.main (); + chosen_file + end let instance = diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 425406a58..a185aaf74 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -46,6 +46,7 @@ class gui : method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin method proof : MatitaGeneratedGui.proofWin + method script: MatitaGeneratedGui.scriptWin method toolbar : MatitaGeneratedGui.toolBarWin (** {2 Access to GUI useful components} *) @@ -61,6 +62,8 @@ class gui : method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + method chooseFile: unit -> string option + end (** singleton instance of the gui *) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 3e505c28e..17a055174 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -84,6 +84,7 @@ class virtual interpreterState ~(console: MatitaConsole.console) = (CicAst.term, string) TacticAst.tactical -> state_tag method evalPhrase s = self#evalTactical (self#parsePhrase s) + end let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy @@ -285,19 +286,39 @@ class interpreter new commandState ~disambiguator ~proof_handler ~console () in let proofState = new proofState ~disambiguator ~proof_handler ~console () in - object + object (self) val mutable state = commandState method reset = state <- commandState + method private updateState = function + | Some `Command -> state <- commandState + | Some `Proof -> state <- proofState + | None -> () + method evalPhrase s = try - (match state#evalPhrase s with - | Some `Command -> state <- commandState - | Some `Proof -> state <- proofState - | None -> ()) + self#updateState (state#evalPhrase s) with exn -> console#echo_error (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) + +(* + method evalAll s = + let get_end_pos = function + | TacticAst.LocatedTactical ((_, end_pos), _) -> end_pos.Lexing.pos_cnum + | _ -> assert false + in + let str_len = String.length s in + let rec aux offset = + let tactical = + self#parsePhrase (String.sub s offset (str_len - offset)) + in + self#updateState (state#evalTactical tactical); + let next_offset = get_end_pos tactical + offset in + if next_offset = str_len - 1 then + in +*) + end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index c0da0447d..092362229 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -54,7 +54,9 @@ class proof_viewer obj = initializer ignore (self#connect#click (fun (gdome_elt, _, _, _) -> match gdome_elt with - | Some gdome_elt -> ignore (self#action_toggle gdome_elt) + | Some gdome_elt -> + prerr_endline (gdome_elt#get_nodeName#to_string); + ignore (self#action_toggle gdome_elt) | None -> ())) val mutable current_infos = None diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml new file mode 100644 index 000000000..f332fcbd1 --- /dev/null +++ b/helm/matita/matitaMisc.ml @@ -0,0 +1,39 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR +let is_regular fname = (Unix.stat fname).Unix.st_kind = Unix.S_REG + +let input_file fname = + let size = (Unix.stat fname).Unix.st_size in + let buf = Buffer.create size in + let ic = open_in fname in + Buffer.add_channel buf ic size; + close_in ic; + Buffer.contents buf + +let is_proof_script fname = true (** TODO Zack *) +let is_proof_object fname = true (** TODO Zack *) + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli new file mode 100644 index 000000000..ae1fc382b --- /dev/null +++ b/helm/matita/matitaMisc.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val is_dir: string -> bool (** @return true if file is a directory *) +val is_regular: string -> bool (** @return true if file is a regular file *) + +val input_file: string -> string (** read all the contents of file to string *) + + (** @return true if file is a (textual) proof script *) +val is_proof_script: string -> bool + + (** @return true if file is a (binary) proof object *) +val is_proof_object: string -> bool + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 86e77e7e8..bea4377e6 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -121,7 +121,19 @@ type proof_handler = class type interpreter = object method reset: unit (** return the interpreter to the initial state *) + + (** parse a single phrase contained in the input string. Additional + * garbage at the end of the phrase is ignored *) method evalPhrase: string -> unit + +(* + (** eval zero or more phrases contained in the input string. Additional + * garbage contained at the end of the last phrase is ignored. + * @return offset from the beginning of the string pointing to the end of + * the last parsed phrase. Next invocations of evalAll should start from + * there *) + method evalAll: string -> int +*) end (** {2 MathML widgets} *)