-matitaCicMisc.cmo: matitaTypes.cmi
-matitaCicMisc.cmx: matitaTypes.cmx
+matitaCicMisc.cmo: matitaTypes.cmi matitaCicMisc.cmi
+matitaCicMisc.cmx: matitaTypes.cmx matitaCicMisc.cmi
matitac.cmo: matitaTypes.cmi matitaProof.cmi matitaInterpreter.cmi \
matitaDisambiguator.cmi buildTimeConf.cmo
matitac.cmx: matitaTypes.cmx matitaProof.cmx matitaInterpreter.cmx \
matitaConsole.cmi buildTimeConf.cmo matitaGui.cmi
matitaGui.cmx: matitaMisc.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
matitaConsole.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaInterpreter.cmi
-matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaInterpreter.cmi
-matitaMathView.cmo: matitaTypes.cmi matitaGui.cmi matitaCicMisc.cmo \
- matitaMathView.cmi
-matitaMathView.cmx: matitaTypes.cmx matitaGui.cmx matitaCicMisc.cmx \
- matitaMathView.cmi
+matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaCicMisc.cmi \
+ matitaInterpreter.cmi
+matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaCicMisc.cmx \
+ matitaInterpreter.cmi
+matitaMathView.cmo: matitaTypes.cmi matitaMisc.cmi matitaGui.cmi \
+ matitaGtkMisc.cmi matitaCicMisc.cmi buildTimeConf.cmo matitaMathView.cmi
+matitaMathView.cmx: matitaTypes.cmx matitaMisc.cmx matitaGui.cmx \
+ matitaGtkMisc.cmx matitaCicMisc.cmx buildTimeConf.cmx matitaMathView.cmi
matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi
matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \
matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \
matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \
matitaDisambiguator.cmx buildTimeConf.cmx
-matitaProof.cmo: matitaTypes.cmi matitaCicMisc.cmo buildTimeConf.cmo \
+matitaProof.cmo: matitaTypes.cmi matitaCicMisc.cmi buildTimeConf.cmo \
matitaProof.cmi
matitaProof.cmx: matitaTypes.cmx matitaCicMisc.cmx buildTimeConf.cmx \
matitaProof.cmi
matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi
matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi
+matitaCicMisc.cmi: matitaTypes.cmi
matitaConsole.cmi: matitaTypes.cmi
matitaDisambiguator.cmi: matitaTypes.cmi
matitaGtkMisc.cmi: matitaTypes.cmi matitaGeneratedGui.cmi
let version = "0.0.1";;
let undo_history_size = 10;;
let console_history_size = 100;;
+let browser_history_size = 100;;
let gtkrc = "@MATITA_GTKRC@";;
let base_uri = "cic:/matita";;
let phrase_sep = ".";;
+let blank_uri = "about:blank";;
+let current_proof_uri = "about:current_proof";;
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image182">
+ <widget class="GtkImage" id="image224">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<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"/>
</widget>
</child>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image183">
+ <widget class="GtkImage" id="image225">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image184">
+ <widget class="GtkImage" id="image226">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image185">
+ <widget class="GtkImage" id="image227">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image186">
+ <widget class="GtkImage" id="image228">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
</child>
<child>
- <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
+ <widget class="GtkMenuItem" id="NewCicBrowserMenuItem">
<property name="visible">True</property>
- <property name="label" translatable="yes">Show Proof Window</property>
+ <property name="label" translatable="yes">New Cic Browser</property>
<property name="use_underline">True</property>
- <property name="active">False</property>
<accelerator key="F3" modifiers="0" signal="activate"/>
</widget>
</child>
- <child>
- <widget class="GtkCheckMenuItem" id="ShowCheckMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Show Check Window</property>
- <property name="use_underline">True</property>
- <property name="active">False</property>
- <accelerator key="F4" modifiers="0" signal="activate"/>
- </widget>
- </child>
-
<child>
<widget class="GtkCheckMenuItem" id="ShowScriptMenuItem">
<property name="visible">True</property>
<widget class="GtkWindow" id="BrowserWin">
<property name="width_request">400</property>
<property name="height_request">500</property>
+ <property name="visible">True</property>
<property name="title" translatable="yes">Cic browser</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
<property name="above_child">False</property>
<child>
- <widget class="GtkVBox" id="vbox7">
+ <widget class="GtkVBox" id="BrowserVBox">
<property name="visible">True</property>
<property name="homogeneous">False</property>
<property name="spacing">0</property>
<property name="homogeneous">False</property>
<property name="spacing">0</property>
+ <child>
+ <widget class="GtkButton" id="BrowserNewButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</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="image191">
+ <property name="visible">True</property>
+ <property name="stock">gtk-new</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>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
<child>
<widget class="GtkButton" id="BrowserBackButton">
<property name="visible">True</property>
</packing>
</child>
+ <child>
+ <widget class="GtkButton" id="BrowserRefreshButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</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="image229">
+ <property name="visible">True</property>
+ <property name="stock">gtk-refresh</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>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
<child>
<widget class="GtkButton" id="BrowserHomeButton">
<property name="visible">True</property>
<child>
<widget class="GtkImage" id="image187">
<property name="visible">True</property>
- <property name="stock">gtk-yes</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>
</child>
<child>
- <widget class="GtkComboBoxEntry" id="BrowserUriCombo">
+ <widget class="GtkEntry" id="BrowserUri">
<property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
</widget>
<packing>
<property name="padding">0</property>
let currentProof = new MatitaProof.currentProof
-let proof_viewer = MatitaMathView.proof_viewer_instance ()
let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
let sequents_viewer =
let set_goal goal =
MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
~sequent_viewer ~set_goal ()
let _ = (* attach observers to proof status *)
- let proof_observer _ (status, ()) =
- let ((uri_opt, _, _, _), _) = status in
- proof_viewer#load_proof status;
- in
+ let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
sequents_viewer#reset;
(match goal_opt with
sequents_viewer#goto_sequent goal)
in
currentProof#addObserver sequents_observer;
- currentProof#addObserver proof_observer;
+ currentProof#addObserver browser_observer;
currentProof#connect `Quit (fun () ->
(* quit program, asking for confirmation if needed *)
if not (currentProof#onGoing ()) ||
false);
currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
-let mathViewer = MatitaMathView.mathViewer ()
-let cicBrowser = MatitaMathView.cicBrowser ()
+let currentProof = (currentProof :> MatitaTypes.currentProof)
+let mathViewer =
+ MatitaMathView.mathViewer ~disambiguator
+ ~currentProof:(currentProof :> MatitaTypes.currentProof) ()
let interpreter =
let console = (gui#console :> MatitaTypes.console) in
- let currentProof = (currentProof :> MatitaTypes.currentProof) in
new MatitaInterpreter.interpreter
- ~disambiguator ~currentProof ~console ~mathViewer ~dbd ()
+ ~disambiguator ~currentProof:(currentProof :> MatitaTypes.currentProof)
+ ~console ~mathViewer ~dbd ()
let _ =
let href_callback uri =
let term = CicAst.Uri (UriManager.string_of_uri uri, None) in
ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term)))
in
- proof_viewer#set_href_callback (Some href_callback);
- sequent_viewer#set_href_callback (Some href_callback);
- mathViewer#set_href_callback (Some href_callback)
+ sequent_viewer#set_href_callback (Some href_callback)
(** {2 Script window handling} *)
gui#console#echo_error (sprintf
"Don't know what to do with file: %s\nUnrecognized file format."
f)));
+ ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
+ let currentProof = (currentProof :> MatitaTypes.currentProof) in
+ ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ())));
connect_button gui#script#scriptWinForwardButton script_forward;
connect_button gui#script#scriptWinBackButton script_back;
connect_button gui#script#scriptWinJumpButton script_jump;
let hole = CicAst.UserInput in
let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
let tac_w_term ast _ =
- gui#console#clear ();
+(* gui#console#clear (); *)
gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
gui#main#mainWin#present ()
in
List.iter
(fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
sequent_viewer#get_selected_terms);
- addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ());
+ addDebugItem "refresh all browsers" MatitaMathView.refresh_all_browsers;
end
(** </DEBUGGING> *)
* http://helm.cs.unibo.it/
*)
+open Printf
+
(** create a Cic.CurrentProof from a given proof *)
let cicCurrentProof (uri, metasenv, bo, ty) =
let uri = MatitaTypes.unopt_uri uri in
(* TODO CSC: Wrong: [] is just plainly wrong *)
Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], [])
+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)
+
+ (** term AST -> Cic.term. Uses disambiguator and change imperatively the
+ * metasenv as needed *)
+let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast =
+ if currentProof#onGoing () then begin
+ let proof = currentProof#proof in
+ let metasenv = proof#metasenv in
+ let goal = proof#goal in
+ let context = canonical_context goal metasenv in
+ let (_, metasenv, term,ugraph) as retval =
+ disambiguator#disambiguateTermAst ~context ~metasenv ast
+ in
+ proof#set_metasenv metasenv;
+ retval
+ end else
+ disambiguator#disambiguateTermAst ast
+
+let get_context_and_metasenv ~(currentProof:MatitaTypes.currentProof) =
+ if currentProof#onGoing () then
+ let proof = currentProof#proof in
+ let metasenv = proof#metasenv in
+ let goal = proof#goal in
+ (canonical_context goal metasenv, metasenv)
+ else
+ ([], [])
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+ (** build a CurrentProof object *)
+val cicCurrentProof:
+ UriManager.uri option * Cic.metasenv * Cic.term * Cic.term ->
+ Cic.obj
+
+ (** build a Constant object *)
+val cicConstant: UriManager.uri option * 'a * Cic.term * Cic.term -> Cic.obj
+
+val canonical_context: int -> (int * 'a * 'b) list -> 'a
+
+ (** term AST -> Cic.term. Uses disambiguator and change imperatively the
+ * metasenv as needed *)
+val disambiguate :
+ disambiguator:MatitaTypes.disambiguator ->
+ currentProof:MatitaTypes.currentProof ->
+ DisambiguateTypes.term ->
+ DisambiguateTypes.environment * Cic.metasenv * Cic.term *
+ CicUniv.universe_graph
+
+val get_context_and_metasenv:
+ currentProof:MatitaTypes.currentProof ->
+ Cic.context * Cic.metasenv
+
type callback = string -> command_outcome
-(* let default_prompt = "# " *)
-let default_prompt = ""
+let default_prompt = "# "
let default_phrase_sep = "."
let default_callback = fun (phrase: string) -> (true, true)
let bullet = "∙"
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) ?evbox ~(paned:GPack.paned) obj
method ignore_insert_text_signal ignore =
_ignore_insert_text_signal <- ignore
- val history = new history BuildTimeConf.console_history_size
+ val history =
+ new MatitaMisc.shell_history BuildTimeConf.console_history_size
val mutable handle_position = 450
val mutable last_phrase = ""
* beginning of user input not yet processed *)
ignore (buf#create_mark ~name:"USER_INPUT_START"
~left_gravity:true buf#start_iter);
+ MatitaGtkMisc.connect_key self#event ~modifiers:[`CONTROL] ~stop:true
+ GdkKeysyms._Return
+ (fun () ->
+ buf#insert ~iter:buf#end_iter "\n";
+ let inserted_text =
+ MatitaMisc.strip_trailing_blanks
+ (buf#get_text
+ ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+ ~stop:buf#end_iter ())
+ in
+ self#invoke_callback inserted_text;
+ self#echo_prompt ());
+
+(*
+ (* callback handling based on phrase terminator (e.g. ";;" at the end of
+ * the row: each time a character is inserted *)
ignore (buf#connect#after#insert_text (fun iter text ->
if (not _ignore_insert_text_signal) &&
(iter#compare buf#end_iter = 0) && (* insertion at end *)
self#invoke_callback inserted_text;
self#echo_prompt ()
end));
+*)
(match evbox with (* history key bindings *)
| None -> ()
| Some evbox ->
(** navigation methods: history, cursor motion, ... *)
method private previous_phrase =
- try self#set_phrase history#previous with History_failure -> ()
+ try self#set_phrase history#previous with MatitaMisc.History_failure -> ()
method private next_phrase =
- try self#set_phrase history#next with History_failure -> ()
+ try self#set_phrase history#next with MatitaMisc.History_failure -> ()
method wrap_exn: 'a. (unit -> 'a) -> 'a option =
fun f ->
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image182 =
+ val image224 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image182" ~info:"GtkImage" xmldata))
- method image182 = image182
+ (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata))
+ method image224 = image224
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 image183 =
+ val image225 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image183" ~info:"GtkImage" xmldata))
- method image183 = image183
+ (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata))
+ method image225 = image225
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image184 =
+ val image226 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image184" ~info:"GtkImage" xmldata))
- method image184 = image184
+ (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata))
+ method image226 = image226
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image185 =
+ val image227 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image185" ~info:"GtkImage" xmldata))
- method image185 = image185
+ (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata))
+ method image227 = image227
val separator1 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
method quitMenuItem = quitMenuItem
- val image186 =
+ val image228 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image186" ~info:"GtkImage" xmldata))
- method image186 = image186
+ (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata))
+ method image228 = image228
val editMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
(Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata))
method showToolBarMenuItem = showToolBarMenuItem
- val showProofMenuItem =
- new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
- (Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
- method showProofMenuItem = showProofMenuItem
- val showCheckMenuItem =
- new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
- (Glade.get_widget_msg ~name:"ShowCheckMenuItem" ~info:"GtkCheckMenuItem" xmldata))
- method showCheckMenuItem = showCheckMenuItem
+ val newCicBrowserMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata))
+ method newCicBrowserMenuItem = newCicBrowserMenuItem
val showScriptMenuItem =
new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
(Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
new GBin.event_box (GtkBin.EventBox.cast
(Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata))
method browserWinEventBox = browserWinEventBox
- val vbox7 =
+ val browserVBox =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata))
- method vbox7 = vbox7
+ (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata))
+ method browserVBox = browserVBox
val hbox7 =
new GPack.box (GtkPack.Box.cast
(Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata))
method hbox7 = hbox7
+ val browserNewButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata))
+ method browserNewButton = browserNewButton
+ val image191 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata))
+ method image191 = image191
val browserBackButton =
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata))
new GMisc.image (GtkMisc.Image.cast
(Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata))
method image189 = image189
+ val browserRefreshButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata))
+ method browserRefreshButton = browserRefreshButton
+ val image229 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata))
+ method image229 = image229
val browserHomeButton =
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata))
new GMisc.image (GtkMisc.Image.cast
(Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata))
method image187 = image187
+ val browserUri =
+ new GEdit.entry (GtkEdit.Entry.cast
+ (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata))
+ method browserUri = browserUri
val frame1 =
new GBin.frame (GtkBin.Frame.cast
(Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata))
val helpMenu_menu : GMenu.menu
val hideConsoleButton : GButton.button
val image169 : GMisc.image
- val image182 : GMisc.image
- val image183 : GMisc.image
- val image184 : GMisc.image
- val image185 : GMisc.image
- val image186 : GMisc.image
+ val image224 : GMisc.image
+ val image225 : GMisc.image
+ val image226 : GMisc.image
+ val image227 : GMisc.image
+ val image228 : 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 newCicBrowserMenuItem : GMenu.menu_item
val newDefsMenuItem : GMenu.menu_item
val newMenu : GMenu.image_menu_item
val newMenu_menu : GMenu.menu
val separator2 : GMenu.menu_item
val separator3 : GMenu.menu_item
val sequentsNotebook : GPack.notebook
- val showCheckMenuItem : GMenu.check_menu_item
val showConsoleMenuItem : GMenu.menu_item
- val showProofMenuItem : GMenu.check_menu_item
val showScriptMenuItem : GMenu.check_menu_item
val showToolBarMenuItem : GMenu.check_menu_item
val toplevel : GWindow.window
method helpMenu_menu : GMenu.menu
method hideConsoleButton : GButton.button
method image169 : GMisc.image
- method image182 : GMisc.image
- method image183 : GMisc.image
- method image184 : GMisc.image
- method image185 : GMisc.image
- method image186 : GMisc.image
+ method image224 : GMisc.image
+ method image225 : GMisc.image
+ method image226 : GMisc.image
+ method image227 : GMisc.image
+ method image228 : 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 newCicBrowserMenuItem : GMenu.menu_item
method newDefsMenuItem : GMenu.menu_item
method newMenu : GMenu.image_menu_item
method newMenu_menu : GMenu.menu
method separator2 : GMenu.menu_item
method separator3 : GMenu.menu_item
method sequentsNotebook : GPack.notebook
- method showCheckMenuItem : GMenu.check_menu_item
method showConsoleMenuItem : GMenu.menu_item
- method showProofMenuItem : GMenu.check_menu_item
method showScriptMenuItem : GMenu.check_menu_item
method showToolBarMenuItem : GMenu.check_menu_item
method toplevel : GWindow.window
val browserBackButton : GButton.button
val browserForwardButton : GButton.button
val browserHomeButton : GButton.button
+ val browserNewButton : GButton.button
+ val browserRefreshButton : GButton.button
+ val browserUri : GEdit.entry
+ val browserVBox : GPack.box
val browserWin : GWindow.window
val browserWinEventBox : GBin.event_box
val frame1 : GBin.frame
val image188 : GMisc.image
val image189 : GMisc.image
val image190 : GMisc.image
+ val image191 : GMisc.image
+ val image229 : GMisc.image
val label10 : GMisc.label
val scrolledBrowser : GBin.scrolled_window
val toplevel : GWindow.window
- val vbox7 : GPack.box
val xml : Glade.glade_xml Gtk.obj
method alignment3 : GBin.alignment
method bind : name:string -> callback:(unit -> unit) -> unit
method browserBackButton : GButton.button
method browserForwardButton : GButton.button
method browserHomeButton : GButton.button
+ method browserNewButton : GButton.button
+ method browserRefreshButton : GButton.button
+ method browserUri : GEdit.entry
+ method browserVBox : GPack.box
method browserWin : GWindow.window
method browserWinEventBox : GBin.event_box
method check_widgets : unit -> unit
method image188 : GMisc.image
method image189 : GMisc.image
method image190 : GMisc.image
+ method image191 : GMisc.image
+ method image229 : GMisc.image
method label10 : GMisc.label
method reparent : GObj.widget -> unit
method scrolledBrowser : GBin.scrolled_window
method toplevel : GWindow.window
- method vbox7 : GPack.box
method xml : Glade.glade_xml Gtk.obj
end
val check_all : ?show:bool -> unit -> unit
let connect_button (button: GButton.button) callback =
ignore (button#connect#clicked callback)
+let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key
+ callback
+=
+ ignore (ev#connect#key_press (fun key' ->
+ let modifiers' = GdkEvent.Key.state key' in
+ (match key' with
+ | key' when GdkEvent.Key.keyval key' = key
+ && List.for_all (fun m -> List.mem m modifiers') modifiers ->
+ callback ();
+ stop
+ | _ -> false)))
+
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 ()));
GtkThread.main ();
(match !interp_no with Some row -> [row] | _ -> raise Cancel)
-let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
+let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () =
let dialog = gui#newConfirmationDialog () in
dialog#confirmationDialog#set_title title;
dialog#confirmationDialogLabel#set_label msg;
ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
connect_button dialog#confirmationDialogOkButton (return true);
connect_button dialog#confirmationDialogCancelButton (return false);
+ if not cancel then dialog#confirmationDialogCancelButton#misc#hide ();
dialog#confirmationDialog#show ();
GtkThread.main ();
(match !result with None -> assert false | Some r -> r)
val connect_button: GButton.button -> (unit -> unit) -> unit
+ (** connect a unit -> unit callback to a particular key press event. Event can
+ * be specified using its keysym and a list of modifiers which must be in
+ * effect for the callback to be executed. Further signal processing of other
+ * key press events remains unchanged; further signal processing of the
+ * specified key press depends on the stop parameter *)
+val connect_key:
+ GObj.event_ops ->
+ ?modifiers:Gdk.Tags.modifier list ->
+ ?stop:bool -> (* stop signal handling when the given key has been pressed?
+ * Defaults to false *)
+ Gdk.keysym -> (* (= int) the key, see GdkKeysyms.ml *)
+ (unit -> unit) -> (* callback *)
+ unit
+
(** single string column list *)
class stringListModel:
GTree.view ->
(** @raise MatitaTypes.Cancel *)
val interactive_interp_choice: gui:#gui -> MatitaTypes.choose_interp_callback
- (** @return true if user hit "ok" button, false if user hit "cancel" button *)
-val ask_confirmation: gui:#gui -> ?title:string -> ?msg:string -> unit -> bool
+ (** @return true if user hit "ok" button, false if user hit "cancel" button
+ * @param cancel if set to true a cancel button is shown to the user, otherwise
+ * it is not (and indeed the function will return true). Defaults to true *)
+val ask_confirmation:
+ gui:#gui ->
+ ?cancel:bool -> ?title:string -> ?msg:string -> unit ->
+ bool
(** @param multiline (default: false) if true a TextView widget will be used
* for prompting the user otherwise a TextEntry widget will be
let proof = new proofWin ~file () in
let check = new checkWin ~file () in
let script = new scriptWin ~file () in
- let browser = new browserWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox;
- check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox;
- browser#browserWinEventBox
- ]
+ check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ]
in
let console =
MatitaConsole.console ~evbox:main#consoleEventBox
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c fileSel; c main; c proof; c toolbar; c check; c script;
- c browser ]);
+ [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
+(*
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
- GdkKeysyms._F5,
+*)
+ [ GdkKeysyms._F5,
toggle_win ~check:main#showScriptMenuItem script#scriptWin;
GdkKeysyms._x, (fun () -> console#toggle ());
];
(* script *)
(* menus *)
toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
+(*
toggle_visibility proof#proofWin main#showProofMenuItem;
toggle_visibility check#checkWin main#showCheckMenuItem;
+*)
toggle_visibility script#scriptWin main#showScriptMenuItem;
List.iter (fun w -> w#misc#set_sensitive false)
[ main#saveMenuItem; main#saveAsMenuItem ];
ignore (main#showConsoleMenuItem#connect#activate console#toggle);
(* main *)
connect_button main#hideConsoleButton console#hide;
-(*
(* console *)
console#echo_message (sprintf "\tMatita version %s\n"
BuildTimeConf.version);
console#echo_prompt ();
console#misc#grab_focus ();
-*)
method about = about
- method browser = browser
method check = check
method console = console
method fileSel = fileSel
method script = script
method toolbar = toolbar
+ method newBrowserWin () =
+ let win = new browserWin ~file () in
+ win#check_widgets ();
+ win
+
method newUriDialog () =
let dialog = new uriChoiceDialog ~file () in
dialog#check_widgets ();
method setQuitCallback : (unit -> unit) -> unit
method setPhraseCallback : (string -> MatitaTypes.command_outcome) -> unit
- (** {2 Access to lower-level GTK widgets} *)
+ (** {2 Access to singleton instances of lower-level GTK widgets} *)
method about : MatitaGeneratedGui.aboutWin
- method browser : MatitaGeneratedGui.browserWin
method check : MatitaGeneratedGui.checkWin
method fileSel : MatitaGeneratedGui.fileSelectionWin
method main : MatitaGeneratedGui.mainWin
* methods below create a new window on each invocation. You should
* remember to destroy windows after use *)
+ method newBrowserWin: unit -> MatitaGeneratedGui.browserWin
method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
| Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
| _ -> assert false
-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)
-
-let get_context_and_metasenv (currentProof:MatitaTypes.currentProof) =
- if currentProof#onGoing () then
- let proof = currentProof#proof in
- let metasenv = proof#metasenv in
- let goal = proof#goal in
- (canonical_context goal metasenv, metasenv)
- else
- ([], [])
-
- (** term AST -> Cic.term. Uses disambiguator and change imperatively the
- * metasenv as needed *)
-let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast =
- if currentProof#onGoing () then begin
- let proof = currentProof#proof in
- let metasenv = proof#metasenv in
- let goal = proof#goal in
- let context = canonical_context goal metasenv in
- let (_, metasenv, term,ugraph) as retval =
- disambiguator#disambiguateTermAst ~context ~metasenv ast
- in
- proof#set_metasenv metasenv;
- retval
- end else
- disambiguator#disambiguateTermAst ast
-
class virtual interpreterState =
(* static values, shared by all states inheriting this class *)
let loc = ref None in
Quiet
| TacticAst.Command (TacticAst.Check term) ->
let (_, _, term,ugraph) =
- disambiguate ~disambiguator ~currentProof term
+ MatitaCicMisc.disambiguate ~disambiguator ~currentProof term
in
- let (context, metasenv) = get_context_and_metasenv currentProof in
+ let (context, metasenv) =
+ MatitaCicMisc.get_context_and_metasenv currentProof
+ in
(* this is the Eval Compute
let term = CicReduction.whd context term in
*)
in
(* TASSI: here ugraph1 is unused.... FIXME *)
let expr = Cic.Cast (term, ty) in
- let sequent = (dummyno, context, expr) in
(match mathViewer with
- | None -> ()
- | Some v -> v#checkTerm sequent metasenv);
+ | Some v -> v#checkTerm (`Cic expr)
+ | _ -> ());
Quiet
| TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->
let uris =
()
=
let disambiguate ast =
- let (_, _, term, _) = disambiguate ~disambiguator ~currentProof ast in
+ let (_, _, term, _) =
+ MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+ in
term
in
(** tactic AST -> ProofEngineTypes.tactic *)
if not b then failwith "Wrong proof";
add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph ();
currentProof#abort ();
- (match mathViewer with None -> () | Some v -> v#unload ());
console#echo_message (sprintf "%s defined" suri);
New_state Command
| TacticAst.Seq tacticals ->
| None -> self#set_selection None
end
-let clickable_math_view =
+let clickable_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
OgtkMathViewProps.set_params
(new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size:None ~log_verbosity:None))
[]
-let clickable_math_view () = clickable_math_view ()
-
-class proof_viewer obj =
- object (self)
-
- inherit clickable_math_view obj
-
- val mutable current_infos = None
- val mutable current_mathml = None
-
- method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
- let uri = unopt_uri uri_opt in
- let obj = cicCurrentProof proof in
- let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
- ids_to_hypotheses,_,_))) =
- ApplyTransformation.mml_of_cic_object uri obj
- in
- current_infos <- Some (ids_to_terms, ids_to_father_ids,
- ids_to_conjectures, ids_to_hypotheses);
- debug_print "load_proof: dumping MathML to ./proof";
- ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
- match current_mathml with
- | None ->
- self#load_root ~root:mathml#get_documentElement ;
- current_mathml <- Some mathml
- | Some current_mathml ->
- self#freeze;
- XmlDiff.update_dom ~from:current_mathml mathml ;
- self#thaw
- end
class sequent_viewer obj =
object(self)
(** constructors *)
+type 'widget constructor =
+ ?hadjustment:GData.adjustment ->
+ ?vadjustment:GData.adjustment ->
+ ?font_size:int ->
+ ?log_verbosity:int ->
+ ?width:int ->
+ ?height:int ->
+ ?packing:(GObj.widget -> unit) ->
+ ?show:bool ->
+ unit ->
+ 'widget
+
let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
~font_size ~log_verbosity))
[]
-class cicBrowser =
- object (self)
- val widget =
- let gui = MatitaGui.instance () in
- sequent_viewer ~show:true ~packing:gui#browser#scrolledBrowser#add ()
+let blank_uri = BuildTimeConf.blank_uri
+let current_proof_uri = BuildTimeConf.current_proof_uri
+exception Browser_failure of string
+
+let cicBrowsers = ref []
+
+class cicBrowser
+ ~(disambiguator:MatitaTypes.disambiguator)
+ ~(currentProof:MatitaTypes.currentProof)
+ ~(history:string MatitaMisc.history)
+ ()
+=
+ let term_RE = Pcre.regexp "^term:(.*)" in
+ let gui = MatitaGui.instance () in
+ let win = gui#newBrowserWin () in
+ let toplevel = win#toplevel in
+ let mathView = sequent_viewer ~packing:win#scrolledBrowser#add () in
+ let fail msg =
+ ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
+ ~title:"Cic browser" ~msg ~cancel:false ());
+ in
+ let handle_error f =
+ try
+ f ()
+ with exn ->
+ fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
+ in
+ object (self)
initializer
- widget#set_href_callback (Some (fun uri -> self#load_uri uri))
+ ignore (win#browserUri#connect#activate (fun () ->
+ self#_loadUri win#browserUri#text));
+ ignore (win#browserHomeButton#connect#clicked (fun () ->
+ self#_loadUri current_proof_uri));
+ ignore (win#browserRefreshButton#connect#clicked self#refresh);
+ ignore (win#browserBackButton#connect#clicked self#back);
+ ignore (win#browserForwardButton#connect#clicked self#forward);
+ ignore (win#toplevel#event#connect#delete (fun _ ->
+ let my_id = Oo.id self in
+ cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+ false));
+ mathView#set_href_callback (Some (fun uri ->
+ handle_error (fun () -> self#_loadUri (UriManager.string_of_uri uri))));
+ self#_loadUri ~add_to_history:false blank_uri;
+ toplevel#show ();
+
+ val mutable current_uri = ""
+ val mutable current_infos = None
+ val mutable current_mathml = None
- method load_uri uri = ()
- end
+ method private back () =
+ try
+ self#_loadUri ~add_to_history:false history#previous
+ with MatitaMisc.History_failure -> ()
-let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
- GtkBase.Widget.size_params
- ~cont:(OgtkMathViewProps.pack_return (fun p ->
- OgtkMathViewProps.set_params
- (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
- ~font_size ~log_verbosity))
- []
+ method private forward () =
+ try
+ self#_loadUri ~add_to_history:false history#next
+ with MatitaMisc.History_failure -> ()
-let proof_viewer_instance =
- let instance = lazy (
- let gui = MatitaGui.instance () in
- proof_viewer ~show:true ~packing:gui#proof#scrolledProof#add ()
- ) in
- fun () -> Lazy.force instance
+ (* loads a uri which can be a cic uri or an about:* uri
+ * @param uri string *)
+ method private _loadUri ?(add_to_history = true) uri =
+ try
+ if current_uri <> uri || uri = current_proof_uri then begin
+ (match uri with
+ | uri when uri = blank_uri -> self#blank ()
+ | uri when uri = current_proof_uri -> self#home ()
+ | uri when Pcre.pmatch ~rex:term_RE uri ->
+ self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1))
+ | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri));
+ self#setUri uri;
+ if add_to_history then history#add uri
+ end
+ with
+ | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri)
+ | CicEnvironment.Object_not_found _ ->
+ fail (sprintf "object not found: %s" uri)
+ | Browser_failure msg -> fail msg
+
+ method loadUri uri =
+ handle_error (fun () -> self#_loadUri ~add_to_history:true uri)
+
+ method private blank () = mathView#load_root MatitaMisc.empty_mathml
+
+ method private home () =
+ if currentProof#onGoing () then
+ self#loadObj (cicCurrentProof currentProof#proof#proof)
+ else
+ raise (Browser_failure "no on going proof")
+
+ (** loads a cic uri from the environment
+ * @param uri UriManager.uri *)
+ method private loadUriManagerUri uri =
+ let uri = UriManager.strip_xpointer uri in
+ let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ self#loadObj obj
+
+ method private setUri uri =
+ win#browserUri#set_text uri;
+ current_uri <- uri
+
+ method private loadObj obj =
+ let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
+ let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+ ids_to_hypotheses,_,_))) =
+ ApplyTransformation.mml_of_cic_object obj
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids,
+ ids_to_conjectures, ids_to_hypotheses);
+ match current_mathml with
+ | Some current_mathml when use_diff ->
+ mathView#freeze;
+ XmlDiff.update_dom ~from:current_mathml mathml;
+ mathView#thaw
+ | _ ->
+ mathView#load_root ~root:mathml#get_documentElement;
+ current_mathml <- Some mathml
-class mathViewer =
- let href_callback: (UriManager.uri -> unit) option ref = ref None in
- object
- val check_widget =
- lazy
- (let gui = MatitaGui.instance () in
- let sequent_viewer =
- sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ()
- in
- sequent_viewer#set_href_callback !href_callback;
- sequent_viewer)
+ method private _loadTerm s =
+ self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s))
- method set_href_callback f = href_callback := f
+ method private _loadTermAst ast =
+ let (_, _, term, _) =
+ MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+ in
+ self#_loadTermCic term
- method checkTerm sequent metasenv =
- let (metano, context, expr) = sequent in
- let widget = Lazy.force check_widget in
- let gui = MatitaGui.instance () in
- gui#check#checkWin#show ();
- gui#main#showCheckMenuItem#set_active true;
- widget#load_sequent (sequent :: metasenv) metano
+ method private _loadTermCic term =
+ let (context, metasenv) =
+ MatitaCicMisc.get_context_and_metasenv currentProof
+ in
+ let dummyno = CicMkImplicit.new_meta metasenv [] in
+ let sequent = (dummyno, context, term) in
+ mathView#load_sequent (sequent :: metasenv) dummyno
+
+ method loadTerm (src:MatitaTypes.term_source) =
+ handle_error (fun () ->
+ (match src with
+ | `Ast ast -> self#_loadTermAst ast
+ | `Cic cic -> self#_loadTermCic cic
+ | `String s -> self#_loadTerm s);
+ self#setUri "check")
+
+ (** {2 methods used by constructor only} *)
+
+ method win = win
+ method history = history
+ method currentUri = current_uri
+ method refresh () =
+ if current_uri = current_proof_uri then
+ self#_loadUri ~add_to_history:false current_proof_uri
- method unload () = (proof_viewer_instance ())#unload
end
let sequents_viewer ~(notebook:GPack.notebook)
=
new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
-let mathViewer () = new mathViewer
+let cicBrowser ~disambiguator ~currentProof () =
+ let size = BuildTimeConf.browser_history_size in
+ let rec aux history =
+ let browser = new cicBrowser ~disambiguator ~currentProof ~history () in
+ let win = browser#win in
+ ignore (win#browserNewButton#connect#clicked (fun () ->
+ let history =
+ new MatitaMisc.browser_history ~memento:history#save size ""
+ in
+ let newBrowser = aux history in
+ newBrowser#loadUri browser#currentUri));
+(*
+ (* attempt (failed) to close windows on CTRL-W ... *)
+ MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
+ GdkKeysyms._W (fun () -> win#toplevel#destroy ());
+*)
+ cicBrowsers := browser :: !cicBrowsers;
+ (browser :> MatitaTypes.cicBrowser)
+ in
+ let history = new MatitaMisc.browser_history size blank_uri in
+ aux history
+
+let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
+
+class mathViewer ~disambiguator ~currentProof =
+ object
+ method checkTerm (src:MatitaTypes.term_source) =
+ let browser = cicBrowser ~disambiguator ~currentProof () in
+ browser#loadTerm src
+ end
-let cicBrowser () = new cicBrowser
+let mathViewer ~disambiguator ~currentProof () =
+ new mathViewer ~disambiguator ~currentProof
method set_href_callback: (UriManager.uri -> unit) option -> unit
end
-class type proof_viewer =
- object
- inherit clickable_math_view
-
- method load_proof: StatefulProofEngine.proof_status -> unit
- end
-
class type sequent_viewer =
object
inherit clickable_math_view
method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
end
-class type cicBrowser =
- object
- method load_uri: UriManager.uri -> unit
- end
-
(** {2 Constructors} *)
-val proof_viewer:
+ (** meta constructor *)
+type 'widget constructor =
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
?font_size:int ->
?packing:(GObj.widget -> unit) ->
?show:bool ->
unit ->
- proof_viewer
+ 'widget
-val sequent_viewer:
- ?hadjustment:GData.adjustment ->
- ?vadjustment:GData.adjustment ->
- ?font_size:int ->
- ?log_verbosity:int ->
- ?width:int ->
- ?height:int ->
- ?packing:(GObj.widget -> unit) ->
- ?show:bool ->
- unit ->
- sequent_viewer
+val clickable_math_view: clickable_math_view constructor
+
+val sequent_viewer: sequent_viewer constructor
val sequents_viewer:
notebook:GPack.notebook ->
unit ->
sequents_viewer
-val cicBrowser: unit -> cicBrowser
-
-val mathViewer: unit -> MatitaTypes.mathViewer
+val cicBrowser:
+ disambiguator:MatitaTypes.disambiguator ->
+ currentProof:MatitaTypes.currentProof ->
+ unit ->
+ MatitaTypes.cicBrowser
-(** {2 Singletons} *)
+val refresh_all_browsers: unit -> unit
- (** singleton proof_viewer instance.
- * Uses singleton GUI instance *)
-val proof_viewer_instance: unit -> proof_viewer
+val mathViewer:
+ disambiguator:MatitaTypes.disambiguator ->
+ currentProof:MatitaTypes.currentProof ->
+ unit ->
+ MatitaTypes.mathViewer
let rex = Pcre.regexp "\\s*$" in
fun s -> Pcre.replace ~rex s
+let empty_mathml =
+ let doc =
+ Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns)
+ ~qualifiedName:(Gdome.domString "math") ~doctype:None
+ in
+ doc#get_documentElement
+
+exception History_failure
+
+type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *)
+
+class type ['a] history =
+ object
+ method add : 'a -> unit
+ method next : 'a
+ method previous : 'a
+ method load: 'a memento -> unit
+ method save: 'a memento
+ end
+
+class shell_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 (self)
+ 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)
+ method load (data', hd', tl', cur') =
+ assert (Array.length data = Array.length data');
+ hd <- hd'; tl <- tl'; cur <- cur';
+ Array.blit data' 0 data 0 (Array.length data')
+ method save = (Array.copy data, hd, tl, cur)
+ end
+
+class ['a] browser_history ?memento size init =
+ object (self)
+ initializer match memento with Some m -> self#load m | _ -> ()
+ val data = Array.create size init
+ val mutable hd = 0
+ val mutable tl = 0
+ val mutable cur = 0
+ method previous =
+ if cur = tl then raise History_failure;
+ cur <- cur - 1;
+ if cur = ~-1 then cur <- size - 1;
+ data.(cur)
+ method next =
+ if cur = hd then raise History_failure;
+ cur <- cur + 1;
+ if cur = size then cur <- 0;
+ data.(cur)
+ method add (e:'a) =
+ cur <- cur + 1;
+ if cur = size then cur <- 0;
+ if cur = tl then tl <- tl + 1;
+ if tl = size then tl <- 0;
+ hd <- cur;
+ data.(cur) <- e
+ method load (data', hd', tl', cur') =
+ assert (Array.length data = Array.length data');
+ hd <- hd'; tl <- tl'; cur <- cur';
+ Array.blit data' 0 data 0 (Array.length data')
+ method save = (Array.copy data, hd, tl, cur)
+ end
+
val strip_trailing_blanks: string -> string
+ (** Gdome.element of a MathML document whose rendering should be blank. Used
+ * by cicBrowser to render "about:blank" document *)
+val empty_mathml: Gdome.element
+
+exception History_failure
+
+type 'a memento
+
+class type ['a] history =
+ object ('b)
+ method add : 'a -> unit
+ method next : 'a (** @raise History_failure *)
+ method previous : 'a (** @raise History_failure *)
+ method load: 'a memento -> unit
+ method save: 'a memento
+ end
+
+ (** shell like history: new items added at the end of the history
+ * @param size maximum history size *)
+class shell_history : int -> [string] history
+
+ (** browser like history: new items added at the current point of the history
+ * @param size maximum history size
+ * @param first element in history (this history is never empty) *)
+class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history
+
| CicTextualParser2.Parse_error (floc, msg) ->
let (x, y) = CicAst.loc_of_floc floc in
sprintf "parse error at character %d-%d: %s" x y msg
+ | CicEnvironment.Object_not_found uri ->
+ sprintf "object not found: %s" (UriManager.string_of_uri uri)
| exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
exception No_proof
method reset : unit
end
+type term_source =
+ [ `Ast of DisambiguateTypes.term
+ | `Cic of Cic.term
+ | `String of string
+ ]
+
class type mathViewer =
object
- method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
- method unload: unit -> unit
- method set_href_callback: (UriManager.uri -> unit) option -> unit
+ method checkTerm: term_source -> unit
+ end
+
+class type cicBrowser =
+ object
+ method loadUri: string -> unit
+ method loadTerm: term_source -> unit
end
type mml_of_cic_sequent =
(** {2 MathML widgets} *)
+type term_source =
+ [ `Ast of DisambiguateTypes.term
+ | `Cic of Cic.term
+ | `String of string
+ ]
+
class type mathViewer =
object
- method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
- method unload: unit -> unit
- method set_href_callback: (UriManager.uri -> unit) option -> unit
+ method checkTerm: term_source -> unit
+ end
+
+class type cicBrowser =
+ object
+ method loadUri: string -> unit
+ method loadTerm: term_source -> unit
end
type mml_of_cic_sequent =
projects / helm.git / commitdiff