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 \
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 \
let console_history_size = 100;;
let gtkrc = "@MATITA_GTKRC@";;
let base_uri = "cic:/matita";;
+module DB = @DBI_MODULE@;;
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 \
fi
MATITA_GTKRC="matita.gtkrc"
+DBI_MODULE="Dbi_$DBI_DRIVER"
AC_SUBST(CAMLP4O)
AC_SUBST(DEBUG)
AC_SUBST(LABLGLADECC)
AC_SUBST(OCAMLFIND)
AC_SUBST(MATITA_GTKRC)
+AC_SUBST(DBI_MODULE)
AC_OUTPUT([
buildTimeConf.ml
<key name="glade_file">matita.glade</key>
<key name="auto_disambiguation">true</key>
</section>
- <section name="mathql_interpreter">
- <key name="db_map">mathql_db_map.txt</key>
- <section name="mysql_connection">
- <key name="host">mowgli.cs.unibo.it</key>
-<!-- <key name="host">localhost</key> -->
- <key name="database">mowgli</key>
- <!-- <key name="port"></key> -->
- <!-- <key name="password"></key> -->
- <key name="user">helm</key>
- </section>
- <key name="postgresql_connection_string">dbname=mowgli host=mowgli.cs.unibo.it user=helm</key>
- <!-- flags is a string of the following characters: -->
- <!-- "P", "Q", "R", "S", "T", "W" -->
- <!-- P selects the PostgreSQL database -->
- <!-- The default database is MySQL -->
- <!-- Q logs the low-level queries (in SQL) -->
- <!-- R logs the result of the executed queries (in MathQL) -->
- <!-- S logs the source of the executed queries (in MathQL) -->
- <!-- T logs statistical information (query execution times) -->
- <!-- W logs some warnings (for mathql experts only) -->
- <!-- By default the above information is not logged -->
- <key name="flags"></key>
+ <section name="db">
+<!-- <key name="host">mowgli.cs.unibo.it</key> -->
+ <key name="host">localhost</key>
+ <key name="user">helm</key>
+ <key name="database">mowgli</key>
</section>
<section name="getter">
<key name="mode">remote</key>
- <key name="url">http://mowgli.cs.unibo.it:58081/</key>
-<!-- <key name="url">http://localhost:58081/</key> -->
+<!-- <key name="url">http://mowgli.cs.unibo.it:58081/</key> -->
+ <key name="url">http://localhost:58081/</key>
</section>
</helm_registry>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image116">
+ <widget class="GtkImage" id="image128">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image117">
+ <widget class="GtkImage" id="image129">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image118">
+ <widget class="GtkImage" id="image130">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image119">
+ <widget class="GtkImage" id="image131">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image120">
+ <widget class="GtkImage" id="image132">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<accelerator key="F4" modifiers="0" signal="activate"/>
</widget>
</child>
+
+ <child>
+ <widget class="GtkCheckMenuItem" id="ShowScriptMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show Script Window</property>
+ <property name="use_underline">True</property>
+ <property name="active">False</property>
+ <accelerator key="F5" modifiers="0" signal="activate"/>
+ </widget>
+ </child>
</widget>
</child>
</widget>
<property name="show_fileops">True</property>
<child internal-child="cancel_button">
- <widget class="GtkButton" id="cancel_button1">
+ <widget class="GtkButton" id="fileSelCancelButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child internal-child="ok_button">
- <widget class="GtkButton" id="ok_button1">
+ <widget class="GtkButton" id="fileSelOkButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="max_length">0</property>
<property name="text" translatable="yes"></property>
<property name="has_frame">True</property>
- <property name="invisible_char" translatable="yes">*</property>
+ <property name="invisible_char">*</property>
<property name="activates_default">False</property>
</widget>
<packing>
</child>
</widget>
+<widget class="GtkWindow" id="ScriptWin">
+ <property name="title" translatable="yes">Matita: script</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="default_width">300</property>
+ <property name="default_height">800</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkEventBox" id="ScriptWinEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox4">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar1">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem1">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="button5">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">go back 1 phrase</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image133">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-back</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem2">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="button6">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">execute til cursor</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image134">
+ <property name="visible">True</property>
+ <property name="stock">gtk-jump-to</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem3">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="button7">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">go forward 1 phrase</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image135">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-forward</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ScrolledScript">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTextView" id="ScriptTextView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="overwrite">False</property>
+ <property name="accepts_tab">True</property>
+ <property name="justification">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap_mode">GTK_WRAP_NONE</property>
+ <property name="cursor_visible">True</property>
+ <property name="pixels_above_lines">0</property>
+ <property name="pixels_below_lines">0</property>
+ <property name="pixels_inside_wrap">0</property>
+ <property name="left_margin">0</property>
+ <property name="right_margin">0</property>
+ <property name="indent">0</property>
+ <property name="text" translatable="yes"></property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+</widget>
+
</glade-interface>
--- /dev/null
+# 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 "<ctrl>b" { "move-cursor" (logical-positions, -1, 0) }
+ bind "<shift><ctrl>b" { "move-cursor" (logical-positions, -1, 1) }
+ bind "<ctrl>f" { "move-cursor" (logical-positions, 1, 0) }
+ bind "<shift><ctrl>f" { "move-cursor" (logical-positions, 1, 1) }
+
+ bind "<alt>b" { "move-cursor" (words, -1, 0) }
+ bind "<shift><alt>b" { "move-cursor" (words, -1, 1) }
+ bind "<alt>f" { "move-cursor" (words, 1, 0) }
+ bind "<shift><alt>f" { "move-cursor" (words, 1, 1) }
+
+ bind "<ctrl>a" { "move-cursor" (paragraph-ends, -1, 0) }
+ bind "<shift><ctrl>a" { "move-cursor" (paragraph-ends, -1, 1) }
+ bind "<ctrl>e" { "move-cursor" (paragraph-ends, 1, 0) }
+ bind "<shift><ctrl>e" { "move-cursor" (paragraph-ends, 1, 1) }
+
+ bind "<ctrl>w" { "cut-clipboard" () }
+ bind "<ctrl>y" { "paste-clipboard" () }
+
+ bind "<ctrl>d" { "delete-from-cursor" (chars, 1) }
+ bind "<alt>d" { "delete-from-cursor" (word-ends, 1) }
+ bind "<ctrl>k" { "delete-from-cursor" (paragraph-ends, 1) }
+ bind "<alt>backslash" { "delete-from-cursor" (whitespace, 1) }
+
+ bind "<alt>space" { "delete-from-cursor" (whitespace, 1)
+ "insert-at-cursor" (" ") }
+ bind "<alt>KP_Space" { "delete-from-cursor" (whitespace, 1)
+ "insert-at-cursor" (" ") }
+
+ #
+ # Some non-Emacs keybindings people are attached to
+ #
+ bind "<ctrl>u" {
+ "move-cursor" (paragraph-ends, -1, 0)
+ "delete-from-cursor" (paragraph-ends, 1)
+ }
+ bind "<ctrl>h" { "delete-from-cursor" (chars, -1) }
+ bind "<ctrl>w" { "delete-from-cursor" (word-ends, -1) }
+}
+
+#
+# Bindings for GtkTextView
+#
+binding "gtk-emacs-text-view"
+{
+# bind "<ctrl>p" { "move-cursor" (display-lines, -1, 0) }
+ bind "<shift><ctrl>p" { "move-cursor" (display-lines, -1, 1) }
+# bind "<ctrl>n" { "move-cursor" (display-lines, 1, 0) }
+ bind "<shift><ctrl>n" { "move-cursor" (display-lines, 1, 1) }
+
+ bind "<ctrl>space" { "set-anchor" () }
+ bind "<ctrl>KP_Space" { "set-anchor" () }
+}
+
+#
+# Bindings for GtkTreeView
+#
+binding "gtk-emacs-tree-view"
+{
+ bind "<ctrl>s" { "start-interactive-search" () }
+ bind "<ctrl>f" { "move-cursor" (logical-positions, 1) }
+ bind "<ctrl>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"
+
open Printf
open MatitaGtkMisc
+open MatitaTypes
+open MatitaMisc
+
+module DB = BuildTimeConf.DB
(** {2 Internal status} *)
(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)
()
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)))
(** <DEBUGGING> *)
+
+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 ();
addDebugItem "dump proof status to stdout" (fun _ ->
print_endline ((get_proof ())#toString));
end
+
(** </DEBUGGING> *)
let _ = GtkThread.main ()
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, ... *)
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 =
| 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
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 ->
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))
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))
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))
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))
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*) () =
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 ();
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
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
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
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
?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
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
open MatitaGeneratedGui
open MatitaGtkMisc
+open MatitaMisc
class gui file =
(* creation order _is_ relevant for windows placement *)
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 :> <check_widgets: unit -> 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));
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 ];
method fileSel = fileSel
method main = main
method proof = proof
+ method script = script
method toolbar = toolbar
method newUriDialog () =
method setPhraseCallback = console#set_callback
+ method chooseFile () =
+ fileSel#fileSelectionWin#show ();
+ GtkThread.main ();
+ chosen_file
+
end
let instance =
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} *)
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+ method chooseFile: unit -> string option
+
end
(** singleton instance of the gui *)
(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
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
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
--- /dev/null
+(* 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 *)
+
--- /dev/null
+(* 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
+
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} *)
projects / helm.git / commitdiff