-logicalOperations.cmo: logicalOperations.cmi
-logicalOperations.cmx: logicalOperations.cmi
-matitaConsole.cmo: matitaConsole.cmi
-matitaConsole.cmx: matitaConsole.cmi
+matitaConsole.cmo: matitaGtkMisc.cmi matitaConsole.cmi
+matitaConsole.cmx: matitaGtkMisc.cmx matitaConsole.cmi
matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmo matitaGtkMisc.cmi
matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi
-matitaGui.cmo: matitaConsole.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi \
- matitaGui.cmi
-matitaGui.cmx: matitaConsole.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmx \
- matitaGui.cmi
+matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \
+ matitaGtkMisc.cmi matitaGui.cmi
+matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \
+ matitaGtkMisc.cmx matitaGui.cmi
matitaInterpreter.cmo: matitaConsole.cmi matitaProof.cmi matitaTypes.cmo \
matitaInterpreter.cmi
matitaInterpreter.cmx: matitaConsole.cmx matitaProof.cmx matitaTypes.cmx \
matitaMathView.cmo: matitaTypes.cmo matitaMathView.cmi
matitaMathView.cmx: matitaTypes.cmx matitaMathView.cmi
matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \
- matitaGui.cmi matitaInterpreter.cmi matitaProof.cmi matitaTypes.cmo
+ matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaProof.cmi \
+ matitaTypes.cmo
matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \
- matitaGui.cmx matitaInterpreter.cmx matitaProof.cmx matitaTypes.cmx
-matitaProof.cmo: matitaTypes.cmo matitaProof.cmi
-matitaProof.cmx: matitaTypes.cmx matitaProof.cmi
+ matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaProof.cmx \
+ matitaTypes.cmx
+matitaProof.cmo: buildTimeConf.cmo matitaTypes.cmo matitaProof.cmi
+matitaProof.cmx: buildTimeConf.cmx matitaTypes.cmx matitaProof.cmi
matitaTypes.cmo: buildTimeConf.cmo
matitaTypes.cmx: buildTimeConf.cmx
-logicalOperations.cmi: matitaTypes.cmo
matitaDisambiguator.cmi: matitaTypes.cmo
matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo
matitaGui.cmi: matitaConsole.cmi matitaGeneratedGui.cmi
*)
let debug = @DEBUG@;;
-
-module Transformer = @TRANSFORMER_MODULE@;;
+let version = "0.0.1";;
+let history_size = 10;;
FINDLIB_REQUIRES="\
lablgtk2.glade \
+lablgtk2.init \
lablgtkmathview \
pcre \
helm-cic_omdoc \
echo "debugging enabled"
fi
-TRANSFORMER_MODULE=ApplyTransformation
-
AC_SUBST(CAMLP4O)
AC_SUBST(DEBUG)
AC_SUBST(TRANSFORMER_MODULE)
<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="host">mowgli.cs.unibo.it</key> -->
+ <key name="host">localhost</key>
<key name="database">mowgli</key>
<!-- <key name="port"></key> -->
<!-- <key name="password"></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="gravity">GDK_GRAVITY_NORTH_WEST</property>
<child>
- <widget class="GtkVBox" id="MainWinShape">
+ <widget class="GtkEventBox" id="MainWinEventBox">
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
<child>
- <widget class="GtkMenuBar" id="MainMenuBar">
+ <widget class="GtkVBox" id="MainWinShape">
<property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
<child>
- <widget class="GtkMenuItem" id="FileMenu">
+ <widget class="GtkMenuBar" id="MainMenuBar">
<property name="visible">True</property>
- <property name="label" translatable="yes">_File</property>
- <property name="use_underline">True</property>
<child>
- <widget class="GtkMenu" id="FileMenu_menu">
+ <widget class="GtkMenuItem" id="FileMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_File</property>
+ <property name="use_underline">True</property>
<child>
- <widget class="GtkImageMenuItem" id="NewMenu">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_New</property>
- <property name="use_underline">True</property>
+ <widget class="GtkMenu" id="FileMenu_menu">
- <child internal-child="image">
- <widget class="GtkImage" id="image76">
+ <child>
+ <widget class="GtkImageMenuItem" id="NewMenu">
<property name="visible">True</property>
- <property name="stock">gtk-new</property>
- <property name="icon_size">1</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="label" translatable="yes">_New</property>
+ <property name="use_underline">True</property>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image84">
+ <property name="visible">True</property>
+ <property name="stock">gtk-new</property>
+ <property name="icon_size">1</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>
+
+ <child>
+ <widget class="GtkMenu" id="NewMenu_menu">
+
+ <child>
+ <widget class="GtkMenuItem" id="NewProofMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Proof or definition ...</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="NewDefsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
</widget>
</child>
<child>
- <widget class="GtkMenu" id="NewMenu_menu">
+ <widget class="GtkImageMenuItem" id="OpenMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Open...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
- <child>
- <widget class="GtkMenuItem" id="NewProofMenuItem">
+ <child internal-child="image">
+ <widget class="GtkImage" id="image85">
<property name="visible">True</property>
- <property name="label" translatable="yes">_Proof or definition ...</property>
- <property name="use_underline">True</property>
- <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ <property name="stock">gtk-open</property>
+ <property name="icon_size">1</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>
- <child>
- <widget class="GtkMenuItem" id="NewDefsMenuItem">
+ <child>
+ <widget class="GtkImageMenuItem" id="SaveMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Save</property>
+ <property name="use_underline">True</property>
+ <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image86">
<property name="visible">True</property>
- <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
- <property name="use_underline">True</property>
+ <property name="stock">gtk-save</property>
+ <property name="icon_size">1</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>
- </child>
-
- <child>
- <widget class="GtkImageMenuItem" id="OpenMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_Open...</property>
- <property name="use_underline">True</property>
- <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
- <child internal-child="image">
- <widget class="GtkImage" id="image77">
+ <child>
+ <widget class="GtkImageMenuItem" id="SaveAsMenuItem">
<property name="visible">True</property>
- <property name="stock">gtk-open</property>
- <property name="icon_size">1</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="label" translatable="yes">Save _As ...</property>
+ <property name="use_underline">True</property>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image87">
+ <property name="visible">True</property>
+ <property name="stock">gtk-save-as</property>
+ <property name="icon_size">1</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>
- </child>
- <child>
- <widget class="GtkImageMenuItem" id="SaveMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_Save</property>
- <property name="use_underline">True</property>
- <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator1">
+ <property name="visible">True</property>
+ </widget>
+ </child>
- <child internal-child="image">
- <widget class="GtkImage" id="image78">
+ <child>
+ <widget class="GtkImageMenuItem" id="QuitMenuItem">
<property name="visible">True</property>
- <property name="stock">gtk-save</property>
- <property name="icon_size">1</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="label" translatable="yes">_Quit</property>
+ <property name="use_underline">True</property>
+ <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image88">
+ <property name="visible">True</property>
+ <property name="stock">gtk-quit</property>
+ <property name="icon_size">1</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>
</child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="EditMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Edit</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="ViewMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_View</property>
+ <property name="use_underline">True</property>
<child>
- <widget class="GtkImageMenuItem" id="SaveAsMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Save _As ...</property>
- <property name="use_underline">True</property>
+ <widget class="GtkMenu" id="ViewMenu_menu">
- <child internal-child="image">
- <widget class="GtkImage" id="image79">
+ <child>
+ <widget class="GtkCheckMenuItem" id="ShowToolBarMenuItem">
<property name="visible">True</property>
- <property name="stock">gtk-save-as</property>
- <property name="icon_size">1</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="label" translatable="yes">Show Button Bar</property>
+ <property name="use_underline">True</property>
+ <property name="active">True</property>
</widget>
</child>
- </widget>
- </child>
- <child>
- <widget class="GtkMenuItem" id="separator1">
- <property name="visible">True</property>
+ <child>
+ <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show Proof Window</property>
+ <property name="use_underline">True</property>
+ <property name="active">False</property>
+ <accelerator key="F3" modifiers="0" signal="activate"/>
+ </widget>
+ </child>
</widget>
</child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Debug</property>
+ <property name="use_underline">True</property>
<child>
- <widget class="GtkImageMenuItem" id="QuitMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_Quit</property>
- <property name="use_underline">True</property>
- <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ <widget class="GtkMenu" id="DebugMenu_menu">
- <child internal-child="image">
- <widget class="GtkImage" id="image80">
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator2">
<property name="visible">True</property>
- <property name="stock">gtk-quit</property>
- <property name="icon_size">1</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>
</child>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="EditMenu">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_Edit</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="ViewMenu">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_View</property>
- <property name="use_underline">True</property>
<child>
- <widget class="GtkMenu" id="ViewMenu_menu">
+ <widget class="GtkMenuItem" id="HelpMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Help</property>
+ <property name="use_underline">True</property>
<child>
- <widget class="GtkCheckMenuItem" id="ShowToolBarMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Show Button Bar</property>
- <property name="use_underline">True</property>
- <property name="active">True</property>
- </widget>
- </child>
+ <widget class="GtkMenu" id="HelpMenu_menu">
- <child>
- <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Show Proof Window</property>
- <property name="use_underline">True</property>
- <property name="active">False</property>
- <accelerator key="F3" modifiers="0" signal="activate"/>
+ <child>
+ <widget class="GtkMenuItem" id="AboutMenuItem">
+
<property name="visible">True</property>
+ <property name="label" translatable="yes">About...</property>
+
<property name="use_underline">True</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
</child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
<child>
- <widget class="GtkMenuItem" id="DebugMenu">
+ <widget class="GtkVPaned" id="MainVPanes">
<property name="visible">True</property>
- <property name="label" translatable="yes">Debug</property>
- <property name="use_underline">True</property>
+ <property name="can_focus">True</property>
+ <property name="position">450</property>
<child>
- <widget class="GtkMenu" id="DebugMenu_menu">
+ <widget class="GtkScrolledWindow" id="ScrolledSequents">
+ <property name="visible">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="GtkMenuItem" id="separator2">
+ <widget class="GtkViewport" id="viewport1">
<property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+
+ <child>
+ <widget class="GtkNotebook" id="SequentsNotebook">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="show_tabs">True</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_TOP</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">False</property>
+ </packing>
</child>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="HelpMenu">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_Help</property>
- <property name="use_underline">True</property>
<child>
- <widget class="GtkMenu" id="HelpMenu_menu">
+ <widget class="GtkEventBox" id="ConsoleEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
<child>
- <widget class="GtkMenuItem" id="AboutMenuItem">
+ <widget class="GtkScrolledWindow" id="ScrolledConsole">
<property name="visible">True</property>
- <property name="label" translatable="yes">About...</property>
- <property name="use_underline">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <placeholder/>
+ </child>
</widget>
</child>
</widget>
- </child>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkVPaned" id="MainVPanes">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="position">450</property>
-
- <child>
- <widget class="GtkScrolledWindow" id="ScrolledSequents">
- <property name="visible">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>
- <placeholder/>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">True</property>
+ </packing>
</child>
</widget>
<packing>
- <property name="shrink">True</property>
- <property name="resize">False</property>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
</packing>
</child>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledConsole">
+ <widget class="GtkStatusbar" id="MainStatusBar">
<property name="visible">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
- <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
-
- <child>
- <placeholder/>
- </child>
+ <property name="has_resize_grip">True</property>
</widget>
<packing>
- <property name="shrink">True</property>
- <property name="resize">True</property>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
</packing>
</child>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkStatusbar" id="MainStatusBar">
- <property name="visible">True</property>
- <property name="has_resize_grip">True</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
</widget>
</child>
</child>
<child>
- <placeholder/>
+ <widget class="GtkLabel" id="AboutLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes"><b>Matita @VERSION@</b>
+
+<tt>http://helm.cs.unibo.it</tt>
+
+Copyright (C) 2004,
+<i>the HELM team</i></property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">True</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">5</property>
+ <property name="ypad">5</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
</widget>
</child>
* http://helm.cs.unibo.it/
*)
+open Printf
+
open MatitaGtkMisc
(** {2 Internal status} *)
let (get_proof, set_proof, has_proof) =
let (current_proof: MatitaTypes.proof option ref) = ref None in
- ((fun () ->
+ ((fun () -> (* get_proof *)
match !current_proof with
| Some proof -> proof
| None -> failwith "No current proof"),
- (fun proof -> (* TODO Zack: this function should probably be smarter taking
- care also of unregistering notifications subscriber and so on *)
- current_proof := proof),
- (fun () -> !current_proof <> None))
+ (fun proof -> (* set_proof *)
+ current_proof := proof),
+ (fun () -> (* has_proof *)
+ !current_proof <> None))
(** {2 Settings} *)
~chooseInterp:(interactive_interp_choice ~gui)
()
let proof_viewer =
- let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in
-(*
let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
-*)
- MatitaMathView.proof_viewer ~show:true ~packing:(gui#proof#scrolledProof#add) ()
-(*
-let sequent_viewer =
- let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in
- MatitaMathView.sequent_viewer ~mml_of_cic_sequent ~show:true
- ~packing:(gui#main#scrolledSequents#add) ()
-*)
+let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
let new_proof (proof: MatitaTypes.proof) =
- (* TODO Zack a lot:
- * - ids_to_inner_types, ids_to_inner_sorts handling
- * - sequent viewer notification
- *)
let xmldump_observer _ _ = print_endline proof#toString in
let proof_observer _ (status, metadata) =
debug_print "proof_observer";
let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- metadata
+ (fst metadata)
in
let ((uri_opt, _, _, _), _) = status in
let uri = MatitaTypes.unopt_uri uri_opt in
debug_print "apply transformation";
let mathml =
- BuildTimeConf.Transformer.mml_of_cic_object
+ ApplyTransformation.mml_of_cic_object
~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
in
if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml";
proof_viewer#load_proof mathml metadata;
debug_print "/proof_observer"
in
+ let sequents_observer =
+ let pages = ref 0 in
+ let callback_id = ref None in
+ let mathmls = ref [] in
+ fun _ ((proof, goal_opt) as status, metadata) ->
+ debug_print "sequents_observer";
+ let notebook = gui#main#sequentsNotebook in
+ for i = 1 to !pages do
+ notebook#remove_page 0
+ done;
+ mathmls := [];
+ (match !callback_id with
+ | Some id -> GtkSignal.disconnect notebook#as_widget id
+ | None -> ());
+ if goal_opt <> None then begin
+ let sequents = snd metadata in
+ let sequents_no = List.length sequents in
+ debug_print (sprintf "sequents no: %d" sequents_no);
+ pages := sequents_no;
+ let widget = sequent_viewer#coerce in
+ List.iter
+ (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) ->
+ let tab_label =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+ in
+ notebook#append_page ~tab_label widget;
+ let mathml = lazy
+ (let content_sequent = Cic2content.map_sequent asequent in
+ let pres_sequent =
+ Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
+ in
+ let xmlpres = Box.document_of_box pres_sequent in
+ Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
+ in
+ mathmls := (metano, mathml) :: !mathmls)
+ sequents;
+ mathmls := List.rev !mathmls;
+ let render_page page =
+ let (metano, mathml) = List.nth !mathmls page in
+ sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
+ in
+ callback_id :=
+ (* TODO Zack the "#after" may probably be removed after Luca's fix for
+ * widget not loading documents before being realized *)
+ Some (notebook#connect#after#switch_page ~callback:(fun page ->
+ debug_print "switch_page callback";
+ render_page page));
+ (match goal_opt with
+ | Some goal -> (* current goal available, go to corresponding page *)
+ let page = ref 0 in
+ (try
+ List.iter
+ (fun (metano, _) ->
+ if (metano = goal) then raise Exit;
+ incr page)
+ sequents;
+ with Exit ->
+ debug_print (sprintf "going to page %d" !page);
+ notebook#goto_page !page;
+ render_page !page)
+ | None -> ());
+ end;
+ debug_print "/sequents_observer"
+ in
ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- xmldump_observer);
+ sequents_observer);
ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
proof_observer);
+ ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
+ xmldump_observer);
proof#notify;
set_proof (Some proof)
then
GMain.Main.quit ()
+let abort_proof () =
+ MatitaTypes.not_implemented "Matita.abort_proof"
+
let proof_handler =
{ MatitaTypes.get_proof = get_proof;
- MatitaTypes.set_proof = set_proof;
+ MatitaTypes.abort_proof = abort_proof;
MatitaTypes.has_proof = has_proof;
MatitaTypes.new_proof = new_proof;
MatitaTypes.quit = quit;
let trailing_NL_RE = Pcre.regexp "\n\\s*$"
+exception History_failure
+
+ (** shell like phrase history *)
+class history size =
+ let size = size + 1 in
+ let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
+ let incr x = (x + 1) mod size in
+ object
+ val data = Array.create size ""
+ val mutable hd = 0 (* insertion point *)
+ val mutable tl = -1 (* oldest inserted item *)
+ val mutable cur = -1 (* current item for the history *)
+ method add s =
+ data.(hd) <- s;
+ if tl = -1 then tl <- hd;
+ hd <- incr hd;
+ if hd = tl then tl <- incr tl;
+ cur <- hd
+ method previous =
+ if cur = tl then raise History_failure;
+ cur <- decr cur;
+ data.(cur)
+ method next =
+ if cur = hd then raise History_failure;
+ cur <- incr cur;
+ if cur = hd then "" else data.(cur)
+ end
+
class console
?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
- ?(callback = default_callback)
- obj
+ ?(callback = default_callback) ?evbox obj
=
object (self)
inherit GText.view obj
method phrase_sep = _phrase_sep
method set_phrase_sep sep = _phrase_sep <- sep
+ val mutable _prompt = prompt
+ method prompt = _prompt
+ method set_prompt prompt = _prompt <- prompt
+
val mutable _callback = callback
method set_callback f = _callback <- f
method ignore_insert_text_signal ignore =
_ignore_insert_text_signal <- ignore
-(*
- (* TODO Zack: implement history.
- IDEA: use CTRL-P/N a la emacs.
- ISSUE: per-phrase or per-line history? *)
- val phrases_history = Array.create history_size None
- val mutable history_last_index = -1
- val mutable history_cur_index = -1
-*)
+ val history = new history history_size
initializer
let buf = self#buffer in
let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
self#lock;
- _callback inserted_text;
+ self#invoke_callback inserted_text;
self#echo_prompt ()
- end))
+ end));
+ (match evbox with
+ | None -> ()
+ | Some evbox ->
+ List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
+ [ GdkKeysyms._p, (fun () -> self#previous_phrase);
+ GdkKeysyms._n, (fun () -> self#next_phrase);
+ GdkKeysyms._a, (fun () -> self#beginning_of_phrase);
+ GdkKeysyms._e, (fun () -> self#end_of_phrase);
+ GdkKeysyms._f, (fun () -> self#forward_char);
+ GdkKeysyms._b, (fun () -> self#backward_char);
+ ])
+
+ method private set_phrase phrase =
+ let buf = self#buffer in
+ buf#delete
+ ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+ ~stop:buf#end_iter;
+ 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));
+ _callback phrase
(* lock old text and bump USER_INPUT_START mark *)
method private lock =
(msg ^ "\n");
self#ignore_insert_text_signal false;
self#lock
+
+ (** navigation methods: history, cursor motion, ... *)
+
+ method private previous_phrase =
+ try self#set_phrase history#previous with History_failure -> ()
+ method private next_phrase =
+ try self#set_phrase history#next with History_failure -> ()
+ method private beginning_of_phrase =
+ let buf = self#buffer in
+ buf#place_cursor ~where:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+ method private end_of_phrase =
+ let buf = self#buffer in
+ buf#place_cursor ~where:buf#end_iter
+ method private forward_char =
+ let buf = self#buffer in
+ buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#forward_char
+ method private backward_char =
+ let buf = self#buffer in
+ buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#backward_char
+
end
let console
?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
- ?(callback = default_callback)
+ ?(callback = default_callback) ?evbox
?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
?width ?height ?packing ?show ()
=
?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
?width ?height ?packing ?show ()
in
- new console ~prompt ~phrase_sep ~callback view#as_view
+ new console ~prompt ~phrase_sep ~callback ?evbox view#as_view
* http://helm.cs.unibo.it/
*)
+ (** @param evbox event box to which keyboard shortcuts are registered; no
+ * shortcut will be registered if evbox is not given *)
class console:
?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) ->
- Gtk.text_view Gtk.obj ->
+ ?evbox:GBin.event_box -> Gtk.text_view Gtk.obj ->
object
inherit GText.view
method echo_message : string -> unit
method echo_error : string -> unit
+ method prompt : string
+ method set_prompt : string -> unit
+
method phrase_sep : string
method set_phrase_sep : string -> unit
?prompt:string ->
?phrase_sep:string ->
?callback:(string -> unit) ->
+ ?evbox:GBin.event_box ->
?buffer:GText.buffer ->
?editable:bool ->
new GWindow.window (GtkWindow.Window.cast
(Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
method mainWin = mainWin
+ val mainWinEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata))
+ method mainWinEventBox = mainWinEventBox
val mainWinShape =
new GPack.box (GtkPack.Box.cast
(Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image76 =
+ val image84 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image76" ~info:"GtkImage" xmldata))
- method image76 = image76
+ (Glade.get_widget_msg ~name:"image84" ~info:"GtkImage" xmldata))
+ method image84 = image84
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 image77 =
+ val image85 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image77" ~info:"GtkImage" xmldata))
- method image77 = image77
+ (Glade.get_widget_msg ~name:"image85" ~info:"GtkImage" xmldata))
+ method image85 = image85
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image78 =
+ val image86 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image78" ~info:"GtkImage" xmldata))
- method image78 = image78
+ (Glade.get_widget_msg ~name:"image86" ~info:"GtkImage" xmldata))
+ method image86 = image86
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image79 =
+ val image87 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image79" ~info:"GtkImage" xmldata))
- method image79 = image79
+ (Glade.get_widget_msg ~name:"image87" ~info:"GtkImage" xmldata))
+ method image87 = image87
val separator1 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata))
+ (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
method separator1 = separator1
val quitMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
method quitMenuItem = quitMenuItem
- val image80 =
+ val image88 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image80" ~info:"GtkImage" xmldata))
- method image80 = image80
+ (Glade.get_widget_msg ~name:"image88" ~info:"GtkImage" xmldata))
+ method image88 = image88
val editMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
method debugMenu_menu = debugMenu_menu
val separator2 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"separator2" ~info:"GtkMenuItem" xmldata))
+ (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata))
method separator2 = separator2
val helpMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
(Glade.get_widget_msg ~name:"ScrolledSequents" ~info:"GtkScrolledWindow" xmldata))
method scrolledSequents = scrolledSequents
+ val viewport1 =
+ new GBin.viewport (GtkBin.Viewport.cast
+ (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata))
+ method viewport1 = viewport1
+ val sequentsNotebook =
+ new GPack.notebook (GtkPack.Notebook.cast
+ (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata))
+ method sequentsNotebook = sequentsNotebook
+ val consoleEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
+ method consoleEventBox = consoleEventBox
val scrolledConsole =
new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
(Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata))
(Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
method mainStatusBar = mainStatusBar
method reparent parent =
- mainWinShape#misc#reparent parent;
+ mainWinEventBox#misc#reparent parent;
toplevel#destroy ()
method check_widgets () = ()
end
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata))
method aboutDismissButton = aboutDismissButton
+ val aboutLabel =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"AboutLabel" ~info:"GtkLabel" xmldata))
+ method aboutLabel = aboutLabel
method reparent parent =
dialog_vbox2#misc#reparent parent;
toplevel#destroy ()
unit ->
object
val aboutMenuItem : GMenu.menu_item
+ val consoleEventBox : GBin.event_box
val debugMenu : GMenu.menu_item
val debugMenu_menu : GMenu.menu
val editMenu : GMenu.menu_item
val fileMenu_menu : GMenu.menu
val helpMenu : GMenu.menu_item
val helpMenu_menu : GMenu.menu
- val image76 : GMisc.image
- val image77 : GMisc.image
- val image78 : GMisc.image
- val image79 : GMisc.image
- val image80 : GMisc.image
+ val image84 : GMisc.image
+ val image85 : GMisc.image
+ val image86 : GMisc.image
+ val image87 : GMisc.image
+ val image88 : GMisc.image
val mainMenuBar : GMenu.menu_shell
val mainStatusBar : GMisc.statusbar
val mainVPanes : GPack.paned
val mainWin : GWindow.window
+ val mainWinEventBox : GBin.event_box
val mainWinShape : GPack.box
val newDefsMenuItem : GMenu.menu_item
val newMenu : GMenu.image_menu_item
val scrolledSequents : GBin.scrolled_window
val separator1 : GMenu.menu_item
val separator2 : GMenu.menu_item
+ val sequentsNotebook : GPack.notebook
val showProofMenuItem : GMenu.check_menu_item
val showToolBarMenuItem : GMenu.check_menu_item
val toplevel : GWindow.window
val viewMenu : GMenu.menu_item
val viewMenu_menu : GMenu.menu
+ val viewport1 : GBin.viewport
val xml : Glade.glade_xml Gtk.obj
method aboutMenuItem : GMenu.menu_item
method bind : name:string -> callback:(unit -> unit) -> unit
method check_widgets : unit -> unit
+ method consoleEventBox : GBin.event_box
method debugMenu : GMenu.menu_item
method debugMenu_menu : GMenu.menu
method editMenu : GMenu.menu_item
method fileMenu_menu : GMenu.menu
method helpMenu : GMenu.menu_item
method helpMenu_menu : GMenu.menu
- method image76 : GMisc.image
- method image77 : GMisc.image
- method image78 : GMisc.image
- method image79 : GMisc.image
- method image80 : GMisc.image
+ method image84 : GMisc.image
+ method image85 : GMisc.image
+ method image86 : GMisc.image
+ method image87 : GMisc.image
+ method image88 : GMisc.image
method mainMenuBar : GMenu.menu_shell
method mainStatusBar : GMisc.statusbar
method mainVPanes : GPack.paned
method mainWin : GWindow.window
+ method mainWinEventBox : GBin.event_box
method mainWinShape : GPack.box
method newDefsMenuItem : GMenu.menu_item
method newMenu : GMenu.image_menu_item
method scrolledSequents : GBin.scrolled_window
method separator1 : GMenu.menu_item
method separator2 : GMenu.menu_item
+ method sequentsNotebook : GPack.notebook
method showProofMenuItem : GMenu.check_menu_item
method showToolBarMenuItem : GMenu.check_menu_item
method toplevel : GWindow.window
method viewMenu : GMenu.menu_item
method viewMenu_menu : GMenu.menu
+ method viewport1 : GBin.viewport
method xml : Glade.glade_xml Gtk.obj
end
class proofWin :
unit ->
object
val aboutDismissButton : GButton.button
+ val aboutLabel : GMisc.label
val aboutWin : GWindow.dialog_any
val dialog_action_area2 : GPack.button_box
val dialog_vbox2 : GPack.box
val toplevel : GWindow.dialog_any
val xml : Glade.glade_xml Gtk.obj
method aboutDismissButton : GButton.button
+ method aboutLabel : GMisc.label
method aboutWin : GWindow.dialog_any
method bind : name:string -> callback:(unit -> unit) -> unit
method check_widgets : unit -> unit
end
*)
+open Printf
+
open MatitaGeneratedGui
open MatitaGtkMisc
let fileSel = new fileSelectionWin ~file () in
let proof = new proofWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
- [ toolbar#toolBarEventBox; proof#proofWinEventBox ]
+ [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox ]
+ in
+ let console =
+ MatitaConsole.console ~evbox:main#consoleEventBox
+ ~packing:main#scrolledConsole#add ()
in
- let console = MatitaConsole.console ~packing:main#scrolledConsole#add () in
object (self)
initializer
(* glade's check widgets *)
about#aboutWin#show ()));
ignore (about#aboutDismissButton#connect#clicked (fun _ ->
about#aboutWin#misc#hide ()));
+ about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
+ ~templ:BuildTimeConf.version about#aboutLabel#label);
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false)
[ main#saveMenuItem; main#saveAsMenuItem ];
main#helpMenu#set_right_justified true;
(* console *)
- console#echo_message "\tMatita version 0.0.1\n";
+ console#echo_message (sprintf "\tMatita version %s\n"
+ BuildTimeConf.version);
console#echo_prompt ();
console#misc#grab_focus ()
| tactical -> shared#evalTactical tactical
end
-let rec lookup_tactic = function
- | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
- | TacticAst.Intros (_, names) ->
- let namer =
- (** use names given by the user as long as they are availble, then
- * fallback on default fresh name generator *)
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = Cic.Name (List.nth names !count) in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
- in
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:namer ()
- | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
- | TacticAst.Assumption -> VariousTactics.assumption_tac
- | TacticAst.Contradiction -> NegationTactics.contradiction_tac
- | TacticAst.Exists -> IntroductionTactics.exists_tac
- | TacticAst.Fourier -> FourierR.fourier_tac
- | TacticAst.Left -> IntroductionTactics.left_tac
- | TacticAst.Right -> IntroductionTactics.right_tac
- | TacticAst.Ring -> Ring.ring_tac
- | TacticAst.Split -> IntroductionTactics.split_tac
- | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
-(*
- (* TODO Zack a lot more of tactics to be implemented here ... *)
- | TacticAst.Absurd
- | TacticAst.Apply of 'term
- | TacticAst.Change of 'term * 'term * 'ident option
- | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
- | TacticAst.Cut of 'term
- | TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
- | TacticAst.Elim of 'term * 'term option
- | TacticAst.ElimType of 'term
- | TacticAst.Exact of 'term
- | TacticAst.Fold of reduction_kind * 'term
- | TacticAst.Injection of 'ident
- | TacticAst.Intros of int option * 'ident list
- | TacticAst.LetIn of 'term * 'ident
- | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
- | TacticAst.Replace of 'term * 'term
- | TacticAst.Replace_pattern of 'term pattern * 'term
- | TacticAst.Rewrite of direction * 'term * 'ident option
- | TacticAst.Transitivity of 'term
-*)
- | _ ->
- MatitaTypes.not_implemented "some tactic"
+let canonical_context metano metasenv =
+ try
+ let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
+ context
+ with Not_found ->
+ failwith (sprintf "Can't find canonical context for %d" metano)
+
+ (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+ * names as long as they are available, then it fallbacks to name generation
+ * using FreshNamesGenerator module *)
+let namer_of names =
+ let len = List.length names in
+ let count = ref 0 in
+ fun metasenv context name ~typ ->
+ if !count < len then begin
+ let name = Cic.Name (List.nth names !count) in
+ incr count;
+ name
+ end else
+ FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
(** Implements phrases that should be accepted only in `Proof state, basically
* tacticals *)
~(console: MatitaConsole.console)
()
=
+ (** term AST -> Cic.term. Uses disambiguator and change imperatively the
+ * metasenv as needed *)
+ let disambiguate ast =
+ let proof = proof_handler.MatitaTypes.get_proof () in
+ let metasenv = proof#metasenv in
+ let goal = proof#goal in
+ let context = canonical_context goal metasenv in
+ let (_, metasenv, term) =
+ disambiguator#disambiguateTermAst ~context ~metasenv ast
+ in
+ proof#set_metasenv metasenv;
+ term
+ in
+ (** tactic AST -> ProofEngineTypes.tactic *)
+ let rec lookup_tactic = function
+ | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
+ | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *)
+ PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
+ | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
+ | TacticAst.Assumption -> VariousTactics.assumption_tac
+ | TacticAst.Contradiction -> NegationTactics.contradiction_tac
+ | TacticAst.Exists -> IntroductionTactics.exists_tac
+ | TacticAst.Fourier -> FourierR.fourier_tac
+ | TacticAst.Left -> IntroductionTactics.left_tac
+ | TacticAst.Right -> IntroductionTactics.right_tac
+ | TacticAst.Ring -> Ring.ring_tac
+ | TacticAst.Split -> IntroductionTactics.split_tac
+ | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
+ | TacticAst.Transitivity term ->
+ EqualityTactics.transitivity_tac (disambiguate term)
+ | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
+ | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
+ | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
+ | TacticAst.ElimType term ->
+ EliminationTactics.elim_type_tac (disambiguate term)
+ | TacticAst.Replace (what, with_what) ->
+ EqualityTactics.replace_tac ~what:(disambiguate what)
+ ~with_what:(disambiguate with_what)
+ (*
+ (* TODO Zack a lot more of tactics to be implemented here ... *)
+ | TacticAst.Absurd
+ | TacticAst.Change of 'term * 'term * 'ident option
+ | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+ | TacticAst.Decompose of 'ident * 'ident list
+ | TacticAst.Discriminate of 'ident
+ | TacticAst.Elim of 'term * 'term option
+ | TacticAst.Fold of reduction_kind * 'term
+ | TacticAst.Injection of 'ident
+ | TacticAst.LetIn of 'term * 'ident
+ | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
+ | TacticAst.Replace_pattern of 'term pattern * 'term
+ | TacticAst.Rewrite of direction * 'term * 'ident option
+ *)
+ | _ ->
+ MatitaTypes.not_implemented "some tactic"
+ in
let shared = new sharedState ~disambiguator ~proof_handler ~console () in
object (self)
inherit interpreterState ~console
method evalTactical = function
| TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
| TacticAst.Command TacticAst.Abort ->
- proof_handler.MatitaTypes.set_proof None;
+ proof_handler.MatitaTypes.abort_proof ();
`Command
+ | TacticAst.Command (TacticAst.Undo steps) ->
+ (proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
+ `Proof
+ | TacticAst.Command (TacticAst.Redo steps) ->
+ (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
+ `Proof
| TacticAst.Seq tacticals ->
(* TODO Zack check for proof completed at each step? *)
List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
(* End of the list utility functions *)
-(*
class sequent_viewer obj =
object(self)
| None -> assert false (* "ERROR: No current term!!!" *)
) selections
- method load_sequent metasenv sequent =
- let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
- mml_of_cic_sequent metasenv sequent
- in
- self#load_root ~root:sequent_mml#get_documentElement ;
- current_infos <-
- Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+ method load_sequent (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata)
+ sequent_no
+ =
+ let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_hypotheses)
+ =
+ try
+ List.assoc sequent_no (snd metadata)
+ with Not_found -> assert false
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
+ self#load_root ~root:mml#get_documentElement
end
-*)
class proof_viewer obj =
object(self)
method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) =
let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- metadata
+ (fst metadata)
in
current_infos <-
Some
(** constructors *)
-(*
let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
(new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size ~log_verbosity))
[]
-*)
let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
unit ->
MatitaTypes.proof_viewer
-(*
val sequent_viewer :
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
?show:bool ->
unit ->
MatitaTypes.sequent_viewer
-*)
(* TODO CSC: Wrong: [] is just plainly wrong *)
Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+let init_metadata status =
+ let ((_, metasenv, _, _) as proof, _) = status in
+ let proof_object_metadata = (* compute proof annotations *)
+ Cic2acic.acic_object_of_cic_object (currentProof proof)
+ in
+ let sequents_metadata = (* compute all sequent annotations from scratch *)
+ List.map
+ (fun ((metano, context, term) as sequent) ->
+ (metano, Cic2acic.asequent_of_sequent metasenv sequent))
+ metasenv
+ in
+ (proof_object_metadata, sequents_metadata)
+
+let compute_metadata (old_status, old_metadata) new_status =
+ let ((_, new_metasenv, _, _) as new_proof, _) = new_status in
+ let proof_object_metadata = (* compute proof annotations *)
+ Cic2acic.acic_object_of_cic_object (currentProof new_proof)
+ in
+ let sequents_metadata = (* compute all sequent annotations from scratch *)
+ (** TODO Zack could we reuse some of the annotations from the previous
+ * status to avoid recomputing all of them? uhm ... we have to which
+ * sequents haven't been changed by last tactic applications ... doh! *)
+ List.map
+ (fun ((metano, context, term) as sequent) ->
+ (metano, Cic2acic.asequent_of_sequent new_metasenv sequent))
+ new_metasenv
+ in
+ (proof_object_metadata, sequents_metadata)
+
class proof ?uri ~typ ~metasenv ~body () =
object (self)
inherit [MatitaTypes.hist_metadata]
- StatefulProofEngine.status ?uri ~typ ~body ~metasenv
- (fun proof ->
- Cic2acic.acic_object_of_cic_object (currentProof (fst proof)))
- (fun (old_proof, old_metadata) new_proof ->
- Cic2acic.acic_object_of_cic_object (currentProof (fst new_proof)))
- ()
+ StatefulProofEngine.status
+ ~history_size:BuildTimeConf.history_size ?uri ~typ ~body ~metasenv
+ init_metadata compute_metadata ()
method toXml =
let currentproof = currentProof self#proof in
end
type hist_metadata =
- Cic.annobj *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (Cic.id, string) Hashtbl.t *
- (Cic.id, Cic2acic.anntypes) Hashtbl.t *
- (Cic.id, Cic.conjecture) Hashtbl.t *
- (Cic.id, Cic.hypothesis) Hashtbl.t
+ ( (** proof object part *)
+ (Cic.annobj * (** annotated object *)
+ (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *)
+ (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *)
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t * (** ids_to_inner_types *)
+ (Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t) (** ids_to_hypotheses *)
+ * (** sequents part *)
+ ((int * (** sequent (meta) index *)
+ (Cic.annconjecture * (** annotated conjecture *)
+ (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *)
+ (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t)) (** ids_to_hypotheses *)
+ list)
+ )
class type proof =
object
type proof_handler =
{ get_proof: unit -> proof; (* return current proof or fail *)
- set_proof: proof option -> unit; (* set a proof option as current proof *)
+ abort_proof: unit -> unit;(* abort current proof, cleaning up garbage *)
has_proof: unit -> bool; (* check if a current proof is available or not *)
new_proof: proof -> unit; (* as a set_proof but takes care also to register
observers *)
(string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
Gdome.document
- (** TODO Zack to be reviewed and unified with proof_viewer above *)
class type sequent_viewer =
object
inherit GMathViewAux.multi_selection_math_view
method get_selected_hypotheses: Cic.hypothesis list
(** load a sequent and render it into parent widget *)
- method load_sequent: Cic.metasenv -> Cic.conjecture -> unit
+ method load_sequent: Gdome.document -> hist_metadata -> int -> unit
end
class type proof_viewer =
object
inherit GMathViewAux.single_selection_math_view
- (** @return the annotated cic term and the ids_to_inner_types and
- * ids_to_inner_sorts maps *)
method load_proof: Gdome.document -> hist_metadata -> unit
end
projects / helm.git / commitdiff