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
+matitaMathView.cmo: matitaCicMisc.cmo matitaGui.cmi matitaTypes.cmo \
+ matitaMathView.cmi
+matitaMathView.cmx: matitaCicMisc.cmx matitaGui.cmx matitaTypes.cmx \
+ matitaMathView.cmi
matitaMisc.cmo: matitaMisc.cmi
matitaMisc.cmx: matitaMisc.cmi
matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \
helm-xml \
helm-xmldiff \
helm-cic_textual_parser2 \
-helm-mathql_interpreter \
"
for r in $FINDLIB_REQUIRES
do
<?xml version="1.0" encoding="utf-8"?>
<helm_registry>
+ <section name="prefs">
+ <key name="server">mowgli.cs.unibo.it</key>
+<!-- <key name="server">localhost</key> -->
+ </section>
<section name="matita">
<key name="glade_file">matita.glade</key>
<key name="auto_disambiguation">true</key>
</section>
<section name="db">
- <key name="host">mowgli.cs.unibo.it</key>
-<!-- <key name="host">localhost</key> -->
+ <key name="host">$(prefs.server)</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://$(prefs.server):58081/</key>
</section>
</helm_registry>
</widget>
<widget class="GtkDialog" id="InterpChoiceDialog">
+ <property name="height_request">200</property>
<property name="title" translatable="yes">Interpretation choice</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
<property name="spacing">0</property>
<child>
- <widget class="GtkLabel" id="label6">
+ <widget class="GtkLabel" id="InterpChoiceDialogLabel">
<property name="visible">True</property>
<property name="label" translatable="yes">some informative message here ...</property>
<property name="use_underline">False</property>
</child>
<child>
- <placeholder/>
+ <widget class="GtkScrolledWindow" id="scrolledwindow4">
+ <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_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="InterpChoiceTreeView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
</child>
</widget>
<packing>
<property name="above_child">False</property>
<child>
- <widget class="GtkVBox" id="vbox4">
+ <widget class="GtkNotebook" id="scriptNotebook">
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</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_BOTTOM</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
<child>
- <widget class="GtkToolbar" id="toolbar1">
+ <widget class="GtkVBox" id="vbox4">
<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>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
<child>
- <widget class="GtkToolItem" id="toolitem1">
+ <widget class="GtkToolbar" id="toolbar1">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</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="GtkButton" id="button5">
+ <widget class="GtkToolItem" id="toolitem1">
<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>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkImage" id="image133">
+ <widget class="GtkButton" id="ScriptWinBackButton">
<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>
+ <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>
- </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="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="ScriptWinJumpButton">
+ <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="GtkButton" id="button6">
+ <widget class="GtkToolItem" id="toolitem3">
<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>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkImage" id="image134">
+ <widget class="GtkButton" id="ScriptWinForwardButton">
<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>
+ <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="homogeneous">False</property>
+ <property name="fill">False</property>
</packing>
</child>
<child>
- <widget class="GtkToolItem" id="toolitem3">
+ <widget class="GtkScrolledWindow" id="ScrolledScript">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</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="GtkButton" id="button7">
+ <widget class="GtkTextView" id="ScriptTextView">
<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>
+ <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="expand">False</property>
- <property name="homogeneous">False</property>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
</packing>
</child>
</widget>
<packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label7">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">script</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</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">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
</packing>
</child>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledScript">
+ <widget class="GtkScrolledWindow" id="scrolledwindow3">
<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="shadow_type">GTK_SHADOW_IN</property>
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkTextView" id="ScriptTextView">
+ <widget class="GtkTreeView" id="treeview1">
<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>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
</widget>
</child>
</widget>
<packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label8">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">outline</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</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">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
</packing>
</child>
</widget>
~chooseUris:(interactive_user_uri_choice ~gui)
~chooseInterp:(interactive_interp_choice ~gui)
()
-let proof_viewer =
- let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
- MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
+let proof_viewer = MatitaMathView.proof_viewer_instance ()
let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
let sequents_viewer =
let set_goal goal =
- debug_print (sprintf "Setting goal %d" goal);
if not (has_proof ()) then assert false;
(get_proof ())#set_goal goal
in
let new_proof (proof: MatitaTypes.proof) =
let xmldump_observer _ _ = print_endline proof#toString in
let proof_observer _ (status, ()) =
- debug_print "proof_observer";
let ((uri_opt, _, _, _), _) = status in
- let uri = MatitaTypes.unopt_uri uri_opt in
- debug_print "apply transformation";
proof_viewer#load_proof status;
- debug_print "/proof_observer"
in
let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
sequents_viewer#reset;
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)
Some term
| None -> None
+(** {2 Script window handling} *)
+
+let script_forward _ =
+ let buf = gui#script#scriptTextView#buffer in
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ interpreter#evalPhrase
+ (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
+ gui#lockScript (locked_iter#offset + interpreter#endOffset)
+
+let script_jump _ =
+ let buf = gui#script#scriptTextView#buffer in
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
+ let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
+ let len = String.length raw_text in
+ let rec parse offset =
+ if offset < len then begin
+ interpreter#evalPhrase ~transparent:true
+ (String.sub raw_text offset (len - offset));
+ let new_offset = interpreter#endOffset + offset in
+ gui#lockScript (new_offset + locked_iter#offset);
+ parse new_offset
+ end
+ in
+ try
+ parse 0
+ with CicTextualParser2.Parse_error _ -> ()
+
+let script_back _ = not_implemented "script_back"
+
+let load_script fname =
+ gui#script#scriptTextView#buffer#set_text (input_file fname);
+ gui#script#scriptWin#show ();
+ gui#main#showScriptMenuItem#set_active true
+
+(** {2 GUI callbacks} *)
+
let _ =
gui#setQuitCallback quit;
gui#setPhraseCallback interpreter#evalPhrase;
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);
- gui#script#scriptWin#show ();
- gui#main#showScriptMenuItem#set_active true
+ | Some f when is_proof_script f -> load_script f
| Some f ->
gui#console#echo_error (sprintf
"Don't know what to do with file: %s\nUnrecognized file format."
f)));
+ ignore (gui#script#scriptWinForwardButton#connect#clicked script_forward);
+ ignore (gui#script#scriptWinBackButton#connect#clicked script_back);
+ ignore (gui#script#scriptWinJumpButton#connect#clicked script_jump);
let tac_w_term name tac _ =
match ask_term ~title:name ~msg:("term for " ^ name) () with
| Some term -> (get_proof ())#apply_tactic (tac ~term)
(** </DEBUGGING> *)
-let _ = GtkThread.main ()
+let _ =
+ (try
+ load_script Sys.argv.(1)
+ with Invalid_argument _ -> ());
+ 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#echo_prompt ()
+ self#lock
+(* self#echo_prompt () *)
(** navigation methods: history, cursor motion, ... *)
new GPack.box (GtkPack.Box.cast
(Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
method vbox3 = vbox3
- val label6 =
+ val interpChoiceDialogLabel =
new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"label6" ~info:"GtkLabel" xmldata))
- method label6 = label6
+ (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata))
+ method interpChoiceDialogLabel = interpChoiceDialogLabel
+ val scrolledwindow4 =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledwindow4 = scrolledwindow4
+ val interpChoiceTreeView =
+ new GTree.view (GtkTree.TreeView.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata))
+ method interpChoiceTreeView = interpChoiceTreeView
method reparent parent =
dialog_vbox4#misc#reparent parent;
toplevel#destroy ()
new GBin.event_box (GtkBin.EventBox.cast
(Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata))
method scriptWinEventBox = scriptWinEventBox
+ val scriptNotebook =
+ new GPack.notebook (GtkPack.Notebook.cast
+ (Glade.get_widget_msg ~name:"scriptNotebook" ~info:"GtkNotebook" xmldata))
+ method scriptNotebook = scriptNotebook
val vbox4 =
new GPack.box (GtkPack.Box.cast
(Glade.get_widget_msg ~name:"vbox4" ~info:"GtkVBox" xmldata))
new GButton.toolbar (GtkButton.Toolbar.cast
(Glade.get_widget_msg ~name:"toolbar1" ~info:"GtkToolbar" xmldata))
method toolbar1 = toolbar1
- val button5 =
+ val scriptWinBackButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button5" ~info:"GtkButton" xmldata))
- method button5 = button5
+ (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata))
+ method scriptWinBackButton = scriptWinBackButton
val image133 =
new GMisc.image (GtkMisc.Image.cast
(Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata))
method image133 = image133
- val button6 =
+ val scriptWinJumpButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button6" ~info:"GtkButton" xmldata))
- method button6 = button6
+ (Glade.get_widget_msg ~name:"ScriptWinJumpButton" ~info:"GtkButton" xmldata))
+ method scriptWinJumpButton = scriptWinJumpButton
val image134 =
new GMisc.image (GtkMisc.Image.cast
(Glade.get_widget_msg ~name:"image134" ~info:"GtkImage" xmldata))
method image134 = image134
- val button7 =
+ val scriptWinForwardButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button7" ~info:"GtkButton" xmldata))
- method button7 = button7
+ (Glade.get_widget_msg ~name:"ScriptWinForwardButton" ~info:"GtkButton" xmldata))
+ method scriptWinForwardButton = scriptWinForwardButton
val image135 =
new GMisc.image (GtkMisc.Image.cast
(Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata))
new GText.view (GtkText.View.cast
(Glade.get_widget_msg ~name:"ScriptTextView" ~info:"GtkTextView" xmldata))
method scriptTextView = scriptTextView
+ val label7 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label7" ~info:"GtkLabel" xmldata))
+ method label7 = label7
+ val scrolledwindow3 =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"scrolledwindow3" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledwindow3 = scrolledwindow3
+ val treeview1 =
+ new GTree.view (GtkTree.TreeView.cast
+ (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata))
+ method treeview1 = treeview1
+ val label8 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label8" ~info:"GtkLabel" xmldata))
+ method label8 = label8
method reparent parent =
scriptWinEventBox#misc#reparent parent;
toplevel#destroy ()
val dialog_vbox4 : GPack.box
val interpChoiceCancelButton : GButton.button
val interpChoiceDialog : GWindow.dialog_any
+ val interpChoiceDialogLabel : GMisc.label
val interpChoiceHelpButton : GButton.button
val interpChoiceOkButton : GButton.button
- val label6 : GMisc.label
+ val interpChoiceTreeView : GTree.view
+ val scrolledwindow4 : GBin.scrolled_window
val toplevel : GWindow.dialog_any
val vbox3 : GPack.box
val xml : Glade.glade_xml Gtk.obj
method dialog_vbox4 : GPack.box
method interpChoiceCancelButton : GButton.button
method interpChoiceDialog : GWindow.dialog_any
+ method interpChoiceDialogLabel : GMisc.label
method interpChoiceHelpButton : GButton.button
method interpChoiceOkButton : GButton.button
- method label6 : GMisc.label
+ method interpChoiceTreeView : GTree.view
method reparent : GObj.widget -> unit
+ method scrolledwindow4 : GBin.scrolled_window
method toplevel : GWindow.dialog_any
method vbox3 : GPack.box
method xml : Glade.glade_xml Gtk.obj
?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 label7 : GMisc.label
+ val label8 : GMisc.label
+ val scriptNotebook : GPack.notebook
val scriptTextView : GText.view
val scriptWin : GWindow.window
+ val scriptWinBackButton : GButton.button
val scriptWinEventBox : GBin.event_box
+ val scriptWinForwardButton : GButton.button
+ val scriptWinJumpButton : GButton.button
val scrolledScript : GBin.scrolled_window
+ val scrolledwindow3 : GBin.scrolled_window
val toolbar1 : GButton.toolbar
val toplevel : GWindow.window
+ val treeview1 : GTree.view
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 label7 : GMisc.label
+ method label8 : GMisc.label
method reparent : GObj.widget -> unit
+ method scriptNotebook : GPack.notebook
method scriptTextView : GText.view
method scriptWin : GWindow.window
+ method scriptWinBackButton : GButton.button
method scriptWinEventBox : GBin.event_box
+ method scriptWinForwardButton : GButton.button
+ method scriptWinJumpButton : GButton.button
method scrolledScript : GBin.scrolled_window
+ method scrolledwindow3 : GBin.scrolled_window
method toolbar1 : GButton.toolbar
method toplevel : GWindow.window
+ method treeview1 : GTree.view
method vbox4 : GPack.box
method xml : Glade.glade_xml Gtk.obj
end
* http://helm.cs.unibo.it/
*)
+open Printf
+
+open MatitaTypes
+
let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) =
ignore (check#connect#toggled (fun _ ->
if check#active then win#show () else win#misc#hide ()));
end
+class interpModel =
+ let cols = new GTree.column_list in
+ let id_col = cols#add Gobject.Data.string in
+ let dsc_col = cols#add Gobject.Data.string in
+ let interp_no_col = cols#add Gobject.Data.int in
+ let tree_store = GTree.tree_store cols in
+ let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
+ let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
+ let id_view_col = GTree.view_column ~renderer:id_renderer () in
+ let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
+ fun tree_view choices ->
+ object
+ initializer
+ tree_view#set_model (Some (tree_store :> GTree.model));
+ ignore (tree_view#append_column id_view_col);
+ ignore (tree_view#append_column dsc_view_col);
+ let name_of_interp =
+ (* try to find a reasonable name for an interpretation *)
+ let idx = ref 0 in
+ fun interp ->
+ try
+ List.assoc "0" interp
+ with Not_found ->
+ incr idx; string_of_int !idx
+ in
+ tree_store#clear ();
+ let idx = ref ~-1 in
+ List.iter
+ (fun interp ->
+ incr idx;
+ let interp_row = tree_store#append () in
+ tree_store#set ~row:interp_row ~column:id_col
+ (name_of_interp interp);
+ tree_store#set ~row:interp_row ~column:interp_no_col !idx;
+ List.iter
+ (fun (id, dsc) ->
+ let row = tree_store#append ~parent:interp_row () in
+ tree_store#set ~row ~column:id_col id;
+ tree_store#set ~row ~column:dsc_col dsc;
+ tree_store#set ~row ~column:interp_no_col !idx)
+ interp)
+ choices
+
+ method get_interp_no tree_path =
+ let iter = tree_store#get_iter tree_path in
+ tree_store#get ~row:iter ~column:interp_no_col
+ end
+
let is_var_uri s =
try
String.sub s (String.length s - 4) 4 = ".var"
class type gui =
object
- method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
- method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+ method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
end
exception Cancel
end
let interactive_interp_choice ~(gui:#gui) choices =
- (* TODO Zack implement interactive_interp_choice *)
- MatitaTypes.warning
- "'interactive_interp_choice' not implemented: returning 1st interpretation";
- [0]
+ assert (choices <> []);
+ let dialog = gui#newInterpDialog () in
+ let model = new interpModel dialog#interpChoiceTreeView choices in
+ let interp_len = List.length (List.hd choices) in
+ dialog#interpChoiceDialog#set_title "Interpretation choice";
+ dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+ let interp_no = ref None in
+ let return _ =
+ dialog#interpChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
+ ignore (dialog#interpChoiceOkButton#connect#clicked (fun _ ->
+ match !interp_no with None -> () | Some _ -> return ()));
+ ignore (dialog#interpChoiceCancelButton#connect#clicked return);
+ ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+ interp_no := Some (model#get_interp_no path);
+ return ()));
+ let selection = dialog#interpChoiceTreeView#selection in
+ ignore (selection#connect#changed (fun _ ->
+ match selection#get_selected_rows with
+ | [path] ->
+ debug_print (sprintf "selection: %d" (model#get_interp_no path));
+ interp_no := Some (model#get_interp_no path)
+ | _ -> assert false));
+ dialog#interpChoiceDialog#show ();
+ GtkThread.main ();
+ (match !interp_no with Some row -> [row] | _ -> raise Cancel)
let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
let dialog = gui#newConfirmationDialog () in
class type gui =
object (* minimal gui object requirements *)
- method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
- method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+ method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
end
(** {3 Dialogs} *)
MatitaConsole.console ~evbox:main#consoleEventBox ~phrase_sep:";;"
~packing:main#scrolledConsole#add ()
in
+ let script_buf = script#scriptTextView#buffer in
object (self)
val mutable chosen_file = None
+ (** text mark and tag representing locked part of a script *)
+ val locked_mark =
+ script_buf#create_mark ~name:"locked" ~left_gravity:true
+ script_buf#start_iter
+ val locked_tag =
+ script_buf#create_tag [`BACKGROUND "green"; `EDITABLE false]
+
initializer
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
| `CANCEL -> return None
| `HELP -> ()
| `DELETE_EVENT -> return None));
+ (* script *)
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false)
[ main#saveMenuItem; main#saveAsMenuItem ];
GtkThread.main ();
!text
+ method lockScript offset =
+ let mark = `MARK locked_mark in
+ script_buf#move_mark mark ~where:(script_buf#get_iter_at_char offset);
+ script_buf#remove_tag locked_tag ~start:script_buf#start_iter
+ ~stop:script_buf#end_iter;
+ script_buf#apply_tag locked_tag ~start:script_buf#start_iter
+ ~stop:(script_buf#get_iter_at_mark mark)
+
end
let instance =
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+ (** {2 Utility methods} *)
+
+ (** ask the used to choose a file with the file chooser *)
method chooseFile: unit -> string option
+
+ (** prompt the user for a (multiline) text entry *)
method askText: ?title:string -> ?msg:string -> unit -> string option
+ (** lock script text view from the beginning to the given offset (in UTF-8
+ * characters) *)
+ method lockScript: int -> unit
+
end
(** singleton instance of the gui *)
open Printf
+open MatitaTypes
+
(** None means: "same state as before" *)
type state_tag = [ `Command | `Proof ] option
exception Command_error of string
+(*
let uri name =
UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name)
+*)
+
+let baseuri = ref "cic:/matita"
+let qualify name =
+ let baseuri = !baseuri in
+ if baseuri.[String.length baseuri - 1] = '/' then
+ baseuri ^ name
+ else
+ String.concat "/" [baseuri; name]
let canonical_context metano metasenv =
try
end else
disambiguator#disambiguateTermAst ast
-class virtual interpreterState ~(console: MatitaConsole.console) =
+class virtual interpreterState =
+ (* static values, shared by all states inheriting this class *)
+ let loc = ref None in
+ let history = ref [] in
+ fun ~(console: MatitaConsole.console) ->
object (self)
+
(** eval a toplevel phrase in the current state and return the new state
*)
- method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
+ method parsePhrase s =
+ match CicTextualParser2.parse_tactical (Stream.of_string s) with
+ | (TacticAst.LocatedTactical (loc', tac)) as tactical ->
+ loc := Some loc';
+ (match tac with (* update interpreter history *)
+ | TacticAst.Command (TacticAst.Qed None) ->
+ history := `Qed :: !history
+ | TacticAst.Command (TacticAst.Theorem (_, Some name, _, None)) ->
+ history := `Theorem name :: !history
+ | TacticAst.Command (TacticAst.Qed _)
+ | TacticAst.Command (TacticAst.Theorem _) -> assert false
+ | _ -> history := `Tactic :: !history);
+ tactical
+ | _ -> assert false
method virtual evalTactical:
(CicAst.term, string) TacticAst.tactical -> state_tag
- method evalPhrase s = self#evalTactical (self#parsePhrase s)
+(*
+ method undo ?(steps = 1) () =
+ for i = 1 to steps do
+ match List.hd !history with
+ | `Qed
+ FINQUI
+*)
+
+ method evalPhrase s =
+ debug_print (sprintf "evaluating '%s'" s);
+ self#evalTactical (self#parsePhrase s)
+
+ method endOffset =
+ match !loc with
+ | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum
+ | None -> failwith "MatitaInterpreter: no offset recorded"
end
| TacticAst.Command TacticAst.Proof ->
(* do nothing, just for compatibility with coq syntax *)
Some `Command
+ | TacticAst.Command (TacticAst.Baseuri (Some uri)) ->
+ baseuri := uri;
+ console#echo_message (sprintf "base uri set to \"%s\"" uri);
+ None
+ | TacticAst.Command (TacticAst.Baseuri None) ->
+ console#echo_message (sprintf "base uri is \"%s\"" !baseuri);
+ None
| TacticAst.Command (TacticAst.Check term) ->
let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
let (context, metasenv) = get_context_and_metasenv proof_handler in
method evalTactical = function
| TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
- | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) ->
+ | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
- let uri =
- match name_opt with
- | None -> None
- | Some name -> Some (uri name)
- in
- let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in
+ let uri = UriManager.uri_of_string (qualify name) in
+ let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in
proof_handler.MatitaTypes.new_proof proof;
Some `Proof
| TacticAst.Command TacticAst.Quit ->
| TacticAst.Command (TacticAst.Redo steps) ->
(proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
Some `Proof
- | TacticAst.Command (TacticAst.Qed name_opt) ->
+ | TacticAst.Command (TacticAst.Qed None) ->
(* TODO Zack this function probably should not simply fail with
* Failure, but rather raise some more meaningful exception *)
if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
let proof = proof_handler.MatitaTypes.get_proof () in
- (match name_opt with
- | None -> ()
- | Some name -> proof#set_uri (uri name));
let (uri, metasenv, bo, ty) = proof#proof in
let uri = MatitaTypes.unopt_uri uri in
if metasenv <> [] then failwith "Proof not completed";
CicEnvironment.add_type_checked_term uri
(Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
proof_handler.MatitaTypes.set_proof None;
+ (MatitaMathView.proof_viewer_instance ())#unload;
(* TODO Zack a lot more to be done here:
* - save object to disk in xml format
* - collect metadata
method reset = state <- commandState
+ method endOffset = state#endOffset
+
method private updateState = function
| Some `Command -> state <- commandState
| Some `Proof -> state <- proofState
| None -> ()
- method evalPhrase s =
+ method evalPhrase ?(transparent = false) s =
try
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
-*)
+ if transparent then
+ raise exn
+ else
+ console#echo_error (sprintf "Uncaught exception: %s"
+ (Printexc.to_string exn))
end
inherit GMathViewAux.single_selection_math_view obj
-(* initializer self#set_log_verbosity 3 *)
+ val mutable current_infos = None
+ val mutable current_mathml = None
initializer
ignore (self#connect#click (fun (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
- val mutable current_mathml = None
+ | None -> ()));
+ (* bugfix: until mapping gtkmathview doesn't draw anything *)
+ ignore (self#misc#connect#after#map (fun _ ->
+ match current_mathml with
+ | None -> ()
+ | Some mathml -> self#load_root ~root:mathml#get_documentElement))
method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ());
match current_mathml with
| None ->
- debug_print "no previous MathML";
self#load_root ~root:mathml#get_documentElement ;
current_mathml <- Some mathml
| Some current_mathml ->
- debug_print "Previous MathML available: xmldiffing ...";
- self#freeze ;
+ self#freeze;
XmlDiff.update_dom ~from:current_mathml mathml ;
self#thaw
end
class sequents_viewer ~(notebook:GPack.notebook)
~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
=
+ let tab_label metano =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+ in
object (self)
val mutable pages = 0
val mutable switch_page_callback = None
val mutable page2goal = [] (* associative list: page no -> goal no *)
val mutable goal2page = [] (* the other way round *)
+ val mutable goal2win = [] (* associative list: goal no -> scrolled win *)
val mutable _metasenv = []
method reset =
pages <- 0;
page2goal <- [];
goal2page <- [];
+ goal2win <- [];
_metasenv <- [];
(match switch_page_callback with
| Some id ->
method load_sequents metasenv =
let sequents_no = List.length metasenv in
_metasenv <- metasenv;
- debug_print (sprintf "sequents no: %d" sequents_no);
pages <- sequents_no;
- let widget = sequent_viewer#coerce in
+ let win metano =
+ let w =
+ GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
+ ~show:true ()
+ in
+ let reparent () =
+ match sequent_viewer#misc#parent with
+ | None -> w#add sequent_viewer#coerce
+ | Some _ -> sequent_viewer#misc#reparent w#coerce
+ in
+ goal2win <- (metano, reparent) :: goal2win;
+ w#coerce
+ in
let page = ref 0 in
List.iter
(fun (metano, _, _) ->
page2goal <- (!page, metano) :: page2goal;
goal2page <- (metano, !page) :: goal2page;
incr page;
- let tab_label =
- (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
- in
- notebook#append_page ~tab_label widget)
+ notebook#append_page ~tab_label:(tab_label metano) (win metano))
metasenv;
switch_page_callback <-
- (* 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";
let goal =
try
List.assoc page page2goal
with Not_found -> assert false
in
set_goal goal;
- self#render_page goal))
+ self#render_page ~page ~goal))
- method private render_page goal =
- sequent_viewer#load_sequent _metasenv goal
+ method private render_page ~page ~goal =
+ sequent_viewer#load_sequent _metasenv goal;
+ try
+ List.assoc goal goal2win ()
+ with Not_found -> assert false
method goto_sequent goal =
let page =
with Not_found -> assert false
in
notebook#goto_page page;
- self#render_page goal
+ self#render_page page goal
end
~font_size ~log_verbosity))
[]
+let proof_viewer_instance =
+ let instance = lazy (
+ let gui = MatitaGui.instance () in
+ let frame =
+ GBin.frame ~packing:(gui#proof#scrolledProof#add_with_viewport)
+ ~show:true ()
+ in
+ proof_viewer ~show:true ~packing:(frame#add) ()
+ ) in
+ fun () -> Lazy.force instance
+
let sequents_viewer ~(notebook:GPack.notebook)
~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
=
unit ->
MatitaTypes.proof_viewer
+ (** singleton proof_viewer instance.
+ * Uses singleton GUI instance *)
+val proof_viewer_instance: unit -> MatitaTypes.proof_viewer
+
val sequent_viewer:
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
exception No_proof (** no current proof is available *)
+exception Cancel
+
+(*
let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
| Some uri -> uri
| None ->
(match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri)
+*)
+let unopt_uri = function Some uri -> uri | None -> assert false
class type parserr = (* "parser" is a keyword :-( *)
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
+ * garbage at the end of the phrase is ignored
+ * @param transparent per default the interpreter catch all exceptions ans
+ * prints them in the console. When transparent is set to true exceptions
+ * are flow through. Defaults to false
+ *)
+ method evalPhrase: ?transparent:bool -> string -> unit
+
+ (** offset from the starting of the last string parser by evalPhrase where
+ * parsing stop.
+ * @raise Failure when no offset has been recorded *)
+ method endOffset: int
(*
- (** 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
+ (** undo last steps phrases.
+ * @param steps number of phrases to undo; defaults to 1 *)
+ method undo: ?steps:int -> unit -> unit
*)
+
end
(** {2 MathML widgets} *)
projects / helm.git / commitdiff