let console_history_size = 100;;
let gtkrc = "@MATITA_GTKRC@";;
let base_uri = "cic:/matita";;
+let phrase_sep = ";;";;
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image128">
+ <widget class="GtkImage" id="image164">
<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="image129">
+ <widget class="GtkImage" id="image165">
<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="image130">
+ <widget class="GtkImage" id="image166">
<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="image131">
+ <widget class="GtkImage" id="image167">
<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="image132">
+ <widget class="GtkImage" id="image168">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<accelerator key="F5" modifiers="0" signal="activate"/>
</widget>
</child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator3">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="ShowConsoleMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show console</property>
+ <property name="use_underline">True</property>
+ <accelerator key="x" modifiers="GDK_MOD1_MASK" signal="activate"/>
+ </widget>
+ </child>
</widget>
</child>
</widget>
<property name="position">450</property>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledSequents">
+ <widget class="GtkNotebook" id="SequentsNotebook">
<property name="visible">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="shadow_type">GTK_SHADOW_NONE</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
-
- <child>
- <widget class="GtkViewport" id="viewport1">
- <property name="visible">True</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
-
- <child>
- <widget class="GtkNotebook" id="SequentsNotebook">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="show_tabs">True</property>
- <property name="show_border">True</property>
- <property name="tab_pos">GTK_POS_TOP</property>
- <property name="scrollable">False</property>
- <property name="enable_popup">False</property>
- </widget>
- </child>
- </widget>
- </child>
+ <property name="can_focus">True</property>
+ <property name="show_tabs">True</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_TOP</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
</widget>
<packing>
<property name="shrink">True</property>
<property name="above_child">False</property>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledConsole">
+ <widget class="GtkHBox" id="hbox4">
<property name="visible">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
- <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
<child>
- <placeholder/>
+ <widget class="GtkVBox" id="vbox6">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkButton" id="HideConsoleButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Hide console</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="image169">
+ <property name="visible">True</property>
+ <property name="stock">gtk-close</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>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ScrolledConsole">
+ <property name="visible">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
</child>
</widget>
</child>
<child>
<widget class="GtkScrolledWindow" id="ScrolledProof">
<property name="visible">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
</widget>
<widget class="GtkWindow" id="ToolBarWin">
- <property name="width_request">150</property>
+ <property name="width_request">155</property>
<property name="height_request">450</property>
<property name="visible">True</property>
<property name="title" translatable="yes">Tactics</property>
<child>
<widget class="GtkButton" id="introsButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Intros</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="applyButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Apply</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="exactButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Exact</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="elimButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Elim</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="elimTypeButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">ElimType</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="splitButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Split</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="leftButton">
+ <property name="width_request">25</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Left</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">left</property>
+ <property name="label" translatable="yes">L</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
<child>
<widget class="GtkButton" id="rightButton">
+ <property name="width_request">25</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Right</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">right</property>
+ <property name="label" translatable="yes">R</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
<child>
<widget class="GtkButton" id="existsButton">
+ <property name="width_request">25</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Exists</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="reflexivityButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Reflexivity</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="symmetryButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Symmetry</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="transitivityButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Transitivity</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="assumptionButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Assumption</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">assum</property>
+ <property name="label" translatable="yes">asum</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
<property name="visible_vertical">True</property>
<property name="is_important">False</property>
- <child>
- <widget class="GtkButton" id="searchButton">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Search</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">search</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolItem" id="toolitem19">
- <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="autoButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Auto</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="cutButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Cut</property>
<property name="can_focus">True</property>
<child>
<widget class="GtkButton" id="replaceButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
<property name="tooltip" translatable="yes">Replace</property>
<property name="can_focus">True</property>
<widget class="GtkScrolledWindow" id="ScrolledCheck">
<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="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
~sequent_viewer ~set_goal ()
let new_proof (proof: MatitaTypes.proof) =
- let xmldump_observer _ _ = print_endline proof#toString in
let proof_observer _ (status, ()) =
let ((uri_opt, _, _, _), _) = status in
proof_viewer#load_proof status;
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)
let console = gui#console in
new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
- (** prompt the user for the textual input of a term and disambiguate it *)
-let ask_term ?(title = "term input") ?(msg = "insert term") () =
- match gui#askText ~title ~msg () with
- | Some t ->
- let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in
- 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)
+ if
+ interpreter#evalPhrase
+ (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
+ then
+ gui#lockScript (locked_iter#offset + interpreter#endOffset)
let script_jump _ =
let buf = gui#script#scriptTextView#buffer 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
+ if
+ interpreter#evalPhrase ~transparent:true
+ (String.sub raw_text offset (len - offset));
+ then begin
+ let new_offset = interpreter#endOffset + offset in
+ gui#lockScript (new_offset + locked_iter#offset);
+ parse new_offset
+ end else
+ raise Exit
end
in
try
parse 0
- with CicTextualParser2.Parse_error _ -> ()
+ with Exit -> ()
let script_back _ = not_implemented "script_back"
gui#setQuitCallback quit;
gui#setPhraseCallback interpreter#evalPhrase;
gui#main#debugMenu#misc#hide ();
- ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
- if has_proof () &&
- not (ask_confirmation ~gui
- ~msg:("Proof in progress, are you sure you want to start a new one?")
- ())
- then
- () (* abort new proof process *)
- else
- let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
- let (env, metasenv, expr) =
- disambiguator#disambiguateTerm (Stream.of_string input)
- in
- let proof = MatitaProof.proof ~typ:expr ~metasenv () in
- new_proof proof));
+ ignore (gui#main#newProofMenuItem#connect#activate
+ (gui#console#show ~msg:"theorem "));
ignore (gui#main#openMenuItem#connect#activate (fun _ ->
match gui#chooseFile () with
| None -> ()
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)
- | None -> ()
+ connect_button gui#script#scriptWinForwardButton script_forward;
+ connect_button gui#script#scriptWinBackButton script_back;
+ connect_button gui#script#scriptWinJumpButton script_jump;
+ let module A = TacticAst in
+ 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#show ~msg:(TacticAstPp.pp_tactic ast) ();
+ gui#main#mainWin#present ()
in
- let tac _ tac _ = (get_proof ())#apply_tactic tac in
let tbar = gui#toolbar in
- ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ())));
- ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply));
- ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact));
- ignore (tbar#elimButton#connect#clicked (tac_w_term "elim"
- Tactics.elim_intros_simpl));
- ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type"
- Tactics.elim_type));
- ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split));
- ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left));
- ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right));
- ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists));
- ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity"
- Tactics.reflexivity));
- ignore (tbar#symmetryButton#connect#clicked (tac "symmetry"
- Tactics.symmetry));
- ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity"
- Tactics.transitivity));
- ignore (tbar#assumptionButton#connect#clicked (tac "assumption"
- Tactics.assumption));
- ignore (tbar#cutButton#connect#clicked (tac_w_term "cut"
- (Tactics.cut ?mk_fresh_name_callback:None)));
- ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd)))
+ connect_button tbar#introsButton (tac (A.Intros (None, [])));
+ connect_button tbar#applyButton (tac_w_term (A.Apply hole));
+ connect_button tbar#exactButton (tac_w_term (A.Exact hole));
+ connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None)));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole));
+ connect_button tbar#splitButton (tac A.Split);
+ connect_button tbar#leftButton (tac A.Left);
+ connect_button tbar#rightButton (tac A.Right);
+ connect_button tbar#existsButton (tac A.Exists);
+ connect_button tbar#reflexivityButton (tac A.Reflexivity);
+ connect_button tbar#symmetryButton (tac A.Symmetry);
+ connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
+ connect_button tbar#assumptionButton (tac A.Assumption);
+ connect_button tbar#cutButton (tac_w_term (A.Cut hole));
+ connect_button tbar#autoButton (tac A.Auto)
(** <DEBUGGING> *)
-let save_dom =
- let domImpl = lazy (Gdome.domImplementation ()) in
- fun ~doc ~dest ->
- ignore
- ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ())
-
let _ =
if BuildTimeConf.debug then begin
gui#main#debugMenu#misc#show ();
in
ignore (item#connect#activate callback)
in
- addDebugItem "interactive user uri choice" (fun _ ->
- try
- let uris =
- interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
- ~msg:"messaggio" ~nonvars_button:true
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
- in
- List.iter prerr_endline uris
- with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
addDebugItem "toggle auto disambiguation" (fun _ ->
Helm_registry.set_bool "matita.auto_disambiguation"
(not (Helm_registry.get_bool "matita.auto_disambiguation")));
- addDebugItem "mono line text input" (fun _ ->
- prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
- addDebugItem "multi line text input" (fun _ ->
- prerr_endline
- (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
addDebugItem "dump proof status to stdout" (fun _ ->
print_endline ((get_proof ())#toString));
+ addDebugItem "hide console" gui#console#hide;
+ addDebugItem "show console" gui#console#show;
end
(** </DEBUGGING> *)
* http://helm.cs.unibo.it/
*)
-let default_prompt = "# "
+open Printf
+
+open MatitaTypes
+
+(* let default_prompt = "# " *)
+let default_prompt = ""
let default_phrase_sep = "."
-let default_callback = fun (phrase: string) -> ()
+let default_callback = fun (phrase: string) -> true
let message_props = [ `STYLE `ITALIC ]
let error_props = [ `WEIGHT `BOLD ]
class console
?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
- ?(callback = default_callback) ?evbox obj
+ ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj
=
object (self)
inherit GText.view obj
val history = new history BuildTimeConf.console_history_size
+ val mutable handle_position = 450
+
initializer
let buf = self#buffer in
self#set_wrap_mode `CHAR;
+ self#hide ();
(* create "USER_INPUT_START" mark. This mark will always point to the
* beginning of user input not yet processed *)
ignore (buf#create_mark ~name:"USER_INPUT_START"
history#add (* do not push trailing phrase separator *)
(String.sub phrase 0
(String.length phrase - String.length _phrase_sep));
- _callback phrase
+ if _callback phrase then
+ self#hide ()
+ (* else callback encountered troubles, don't hide console which
+ probably contains error message *)
+
+ method clear () =
+ let buf = self#buffer in
+ buf#delete ~start:buf#start_iter ~stop:buf#end_iter
(* lock old text and bump USER_INPUT_START mark *)
method private lock =
self#lock
method echo_error msg =
+ self#show ();
let buf = self#buffer in
self#ignore_insert_text_signal true;
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 () *)
+
+ method show ?(msg = "") () =
+ self#buffer#insert msg;
+ paned#set_position handle_position;
+ self#misc#grab_focus ()
+ method hide () =
+ self#clear ();
+ paned#set_position max_int
(** navigation methods: history, cursor motion, ... *)
method private next_phrase =
try self#set_phrase history#next with History_failure -> ()
+ method wrap_exn f =
+ try
+ f ()
+ with exn ->
+ self#echo_error (sprintf "Uncaught exception: %s"
+ (Printexc.to_string exn))
+
end
let console
?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep)
- ?(callback = default_callback) ?evbox
+ ?(callback = default_callback) ?evbox ~paned
?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
?width ?height ?packing ?show ()
=
?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width
?width ?height ?packing ?show ()
in
- new console ~prompt ~phrase_sep ~callback ?evbox view#as_view
+ new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
(** @param evbox event box to which keyboard shortcuts are registered; no
* shortcut will be registered if evbox is not given *)
class console:
- ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) ->
- ?evbox:GBin.event_box -> Gtk.text_view Gtk.obj ->
+ ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> bool) ->
+ ?evbox:GBin.event_box -> paned:GPack.paned -> Gtk.text_view Gtk.obj ->
object
inherit GText.view
method echo_prompt : unit -> unit
method echo_message : string -> unit
method echo_error : string -> unit
+ method clear : unit -> unit
+
+ (* console visibility handling inside VPaned *)
+
+ (** @param msg if given, show the console with a prefeed input, cursor
+ * just after it; defaults to the empty string *)
+ method show : ?msg:string -> unit -> unit
+ method hide : unit -> unit
+(* method toggle : unit -> unit *)
method prompt : string
method set_prompt : string -> unit
method set_phrase_sep : string -> unit
(** override previous callback definition *)
- method set_callback : (string -> unit) -> unit
+ method set_callback : (string -> bool) -> unit
method ignore_insert_text_signal: bool -> unit
+
+ (** execute a unit -> unit function, if it raises exceptions shows them as
+ * errors in the console *)
+ method wrap_exn : (unit -> unit) -> unit
end
(** @param prompt user prompt (default "# ")
val console :
?prompt:string ->
?phrase_sep:string ->
- ?callback:(string -> unit) ->
+ ?callback:(string -> bool) ->
?evbox:GBin.event_box ->
+ paned:GPack.paned ->
?buffer:GText.buffer ->
?editable:bool ->
* http://helm.cs.unibo.it/
*)
+open MatitaTypes
+
class parserr () =
object
method parseTerm = CicTextualParser2.parse_term
~nonvars_button:enable_button_for_non_vars uris
let interactive_interpretation_choice = chooseInterp
- let input_or_locate_uri ~(title:string) =
- (* TODO Zack: I try to avoid using this callback. I therefore assume
- * that the presence of an identifier that can't be resolved via
- * "locate" query is a syntax error *)
- MatitaTypes.not_implemented
- "MatitaDisambiguator: input_or_locate_uri callback"
+ let input_or_locate_uri ~(title:string) ?id =
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ let msg = match id with Some id -> id | _ -> "" in
+ raise (Unbound_identifier msg)
end
in
let module Disambiguator = Disambiguate.Make (Callbacks) in
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image128 =
+ val image164 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image128" ~info:"GtkImage" xmldata))
- method image128 = image128
+ (Glade.get_widget_msg ~name:"image164" ~info:"GtkImage" xmldata))
+ method image164 = image164
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 image129 =
+ val image165 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image129" ~info:"GtkImage" xmldata))
- method image129 = image129
+ (Glade.get_widget_msg ~name:"image165" ~info:"GtkImage" xmldata))
+ method image165 = image165
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image130 =
+ val image166 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image130" ~info:"GtkImage" xmldata))
- method image130 = image130
+ (Glade.get_widget_msg ~name:"image166" ~info:"GtkImage" xmldata))
+ method image166 = image166
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image131 =
+ val image167 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image131" ~info:"GtkImage" xmldata))
- method image131 = image131
+ (Glade.get_widget_msg ~name:"image167" ~info:"GtkImage" xmldata))
+ method image167 = image167
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 image132 =
+ val image168 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image132" ~info:"GtkImage" xmldata))
- method image132 = image132
+ (Glade.get_widget_msg ~name:"image168" ~info:"GtkImage" xmldata))
+ method image168 = image168
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:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
method showScriptMenuItem = showScriptMenuItem
+ val separator3 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata))
+ method separator3 = separator3
+ val showConsoleMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata))
+ method showConsoleMenuItem = showConsoleMenuItem
val debugMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
new GPack.paned (GtkPack.Paned.cast
(Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata))
method mainVPanes = mainVPanes
- val scrolledSequents =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"ScrolledSequents" ~info:"GtkScrolledWindow" xmldata))
- method scrolledSequents = scrolledSequents
- val viewport1 =
- new GBin.viewport (GtkBin.Viewport.cast
- (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata))
- method viewport1 = viewport1
val sequentsNotebook =
new GPack.notebook (GtkPack.Notebook.cast
(Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata))
new GBin.event_box (GtkBin.EventBox.cast
(Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
method consoleEventBox = consoleEventBox
+ val hbox4 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox4" ~info:"GtkHBox" xmldata))
+ method hbox4 = hbox4
+ val vbox6 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata))
+ method vbox6 = vbox6
+ val hideConsoleButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata))
+ method hideConsoleButton = hideConsoleButton
+ val image169 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata))
+ method image169 = image169
val scrolledConsole =
new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
(Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata))
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata))
method assumptionButton = assumptionButton
- val searchButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"searchButton" ~info:"GtkButton" xmldata))
- method searchButton = searchButton
val autoButton =
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata))
val editMenu : GMenu.menu_item
val fileMenu : GMenu.menu_item
val fileMenu_menu : GMenu.menu
+ val hbox4 : GPack.box
val helpMenu : GMenu.menu_item
val helpMenu_menu : GMenu.menu
- val image128 : GMisc.image
- val image129 : GMisc.image
- val image130 : GMisc.image
- val image131 : GMisc.image
- val image132 : GMisc.image
+ val hideConsoleButton : GButton.button
+ val image164 : GMisc.image
+ val image165 : GMisc.image
+ val image166 : GMisc.image
+ val image167 : GMisc.image
+ val image168 : GMisc.image
+ val image169 : GMisc.image
val mainMenuBar : GMenu.menu_shell
val mainStatusBar : GMisc.statusbar
val mainVPanes : GPack.paned
val saveAsMenuItem : GMenu.image_menu_item
val saveMenuItem : GMenu.image_menu_item
val scrolledConsole : GBin.scrolled_window
- val scrolledSequents : GBin.scrolled_window
val separator1 : GMenu.menu_item
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
+ val vbox6 : GPack.box
val viewMenu : GMenu.menu_item
val viewMenu_menu : GMenu.menu
- val viewport1 : GBin.viewport
val xml : Glade.glade_xml Gtk.obj
method aboutMenuItem : GMenu.menu_item
method bind : name:string -> callback:(unit -> unit) -> unit
method editMenu : GMenu.menu_item
method fileMenu : GMenu.menu_item
method fileMenu_menu : GMenu.menu
+ method hbox4 : GPack.box
method helpMenu : GMenu.menu_item
method helpMenu_menu : GMenu.menu
- method image128 : GMisc.image
- method image129 : GMisc.image
- method image130 : GMisc.image
- method image131 : GMisc.image
- method image132 : GMisc.image
+ method hideConsoleButton : GButton.button
+ method image164 : GMisc.image
+ method image165 : GMisc.image
+ method image166 : GMisc.image
+ method image167 : GMisc.image
+ method image168 : GMisc.image
+ method image169 : GMisc.image
method mainMenuBar : GMenu.menu_shell
method mainStatusBar : GMisc.statusbar
method mainVPanes : GPack.paned
method saveAsMenuItem : GMenu.image_menu_item
method saveMenuItem : GMenu.image_menu_item
method scrolledConsole : GBin.scrolled_window
- method scrolledSequents : GBin.scrolled_window
method separator1 : GMenu.menu_item
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
+ method vbox6 : GPack.box
method viewMenu : GMenu.menu_item
method viewMenu_menu : GMenu.menu
- method viewport1 : GBin.viewport
method xml : Glade.glade_xml Gtk.obj
end
class proofWin :
val reflexivityButton : GButton.button
val replaceButton : GButton.button
val rightButton : GButton.button
- val searchButton : GButton.button
val splitButton : GButton.button
val symmetryButton : GButton.button
val toolBarEventBox : GBin.event_box
method reparent : GObj.widget -> unit
method replaceButton : GButton.button
method rightButton : GButton.button
- method searchButton : GButton.button
method splitButton : GButton.button
method symmetryButton : GButton.button
method toolBarEventBox : GBin.event_box
open MatitaTypes
+let connect_button (button: GButton.button) callback =
+ ignore (button#connect#clicked callback)
+
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 ()));
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
end
-exception Cancel
-
let interactive_user_uri_choice
~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "")
?(msg = "") ?(nonvars_button=false) uris
GMain.Main.quit ()
in
ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
- ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
- return (Some (Lazy.force nonvars_uris))));
- ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
+ connect_button dialog#uriChoiceConstantsButton (fun _ ->
+ return (Some (Lazy.force nonvars_uris)));
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
Helm_registry.set_bool "matita.auto_disambiguation" true;
- return (Some (Lazy.force nonvars_uris))));
- ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ ->
+ return (Some (Lazy.force nonvars_uris)));
+ connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris)));
- ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None));
+ | uris -> return (Some uris));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
GtkThread.main ();
(match !choices with
dialog#interpChoiceDialog#destroy ();
GMain.Main.quit ()
in
+ let fail _ = interp_no := None; return () 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);
+ connect_button dialog#interpChoiceOkButton (fun _ ->
+ match !interp_no with None -> () | Some _ -> return ());
+ connect_button dialog#interpChoiceCancelButton fail;
ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
interp_no := Some (model#get_interp_no path);
return ()));
GMain.Main.quit ()
in
ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
- ignore (dialog#confirmationDialogOkButton#connect#clicked (return true));
- ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false));
+ connect_button dialog#confirmationDialogOkButton (return true);
+ connect_button dialog#confirmationDialogCancelButton (return false);
dialog#confirmationDialog#show ();
GtkThread.main ();
(match !result with None -> assert false | Some r -> r)
in
let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
view#misc#grab_focus ();
- ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
- return (Some (view#buffer#get_text ()))))
+ connect_button dialog#emptyDialogOkButton (fun _ ->
+ return (Some (view#buffer#get_text ())))
end else begin (* monoline input required: use a TextEntry widget *)
let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in
entry#misc#grab_focus ();
- ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
- return (Some entry#text)))
+ connect_button dialog#emptyDialogOkButton (fun _ ->
+ return (Some entry#text))
end;
- ignore (dialog#emptyDialogCancelButton#connect#clicked (fun _ ->return None));
+ connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
dialog#emptyDialog#show ();
GtkThread.main ();
(match !result with None -> raise Cancel | Some r -> r)
val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit
+val connect_button: GButton.button -> (unit -> unit) -> unit
+
(** single string column list *)
class stringListModel:
GTree.view ->
(** {3 Dialogs} *)
-exception Cancel (* raised when no answer is given by the user *)
-
- (** @raise Cancel *)
+ (** @raise MatitaTypes.Cancel *)
val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback
- (** @raise Cancel *)
+ (** @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 *)
let script = new scriptWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox;
- check#checkWinEventBox; script#scriptWinEventBox ]
+ check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ]
in
let console =
- MatitaConsole.console ~evbox:main#consoleEventBox ~phrase_sep:";;"
- ~packing:main#scrolledConsole#add ()
+ MatitaConsole.console ~evbox:main#consoleEventBox
+ ~phrase_sep:BuildTimeConf.phrase_sep
+ ~packing:main#scrolledConsole#add ~paned:main#mainVPanes ()
in
let script_buf = script#scriptTextView#buffer in
object (self)
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 ]);
- (* show/hide commands *)
- toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
- toggle_visibility proof#proofWin main#showProofMenuItem;
- toggle_visibility check#checkWin main#showCheckMenuItem;
- toggle_visibility script#scriptWin main#showScriptMenuItem;
(* "global" key bindings *)
List.iter (fun (key, callback) -> self#addKeyBinding key callback)
[ GdkKeysyms._F3,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
GdkKeysyms._F5,
toggle_win ~check:main#showScriptMenuItem script#scriptWin;
+ GdkKeysyms._x, (fun () -> console#show ());
];
(* about win *)
ignore (about#aboutWin#event#connect#delete (fun _ -> true));
ignore (main#aboutMenuItem#connect#activate (fun _ ->
about#aboutWin#show ()));
- ignore (about#aboutDismissButton#connect#clicked (fun _ ->
- about#aboutWin#misc#hide ()));
+ connect_button about#aboutDismissButton (fun _ ->
+ about#aboutWin#misc#hide ());
about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
~templ:BuildTimeConf.version about#aboutLabel#label);
(* file selection win *)
| `DELETE_EVENT -> return None));
(* 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 ];
main#helpMenu#set_right_justified true;
+ ignore (main#showConsoleMenuItem#connect#activate console#show);
+ (* 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 ()
+ console#misc#grab_focus ();
+*)
method about = about
method check = check
GMain.Main.quit ()
in
ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
- ignore (dialog#textDialogCancelButton#connect#clicked (fun _ ->
- return None));
- ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+ connect_button dialog#textDialogCancelButton (fun _ -> return None);
+ connect_button dialog#textDialogOkButton (fun _ ->
let text = dialog#textDialogTextView#buffer#get_text () in
- return (Some text)));
+ return (Some text));
dialog#textDialog#show ();
GtkThread.main ();
!text
object
method setQuitCallback : (unit -> unit) -> unit
- method setPhraseCallback : (string -> unit) -> unit
+ method setPhraseCallback : (string -> bool) -> unit
(** {2 Access to lower-level GTK widgets} *)
method virtual evalTactical:
(CicAst.term, string) TacticAst.tactical -> state_tag
-(*
- 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 evalAst ast = self#evalTactical ast
+
method endOffset =
match !loc with
| Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum
new commandState ~disambiguator ~proof_handler ~console ()
in
let proofState = new proofState ~disambiguator ~proof_handler ~console () in
+ let wrap_exn transparent f =
+ try
+ f ();
+ true
+ with exn ->
+ if transparent then
+ raise exn
+ else
+ console#echo_error (sprintf "Uncaught exception: %s"
+ (Printexc.to_string exn));
+ false
+ in
object (self)
val mutable state = commandState
| None -> ()
method evalPhrase ?(transparent = false) s =
- try
- self#updateState (state#evalPhrase s)
- with exn ->
- if transparent then
- raise exn
- else
- console#echo_error (sprintf "Uncaught exception: %s"
- (Printexc.to_string exn))
+ wrap_exn transparent (fun () -> self#updateState (state#evalPhrase s))
+
+ method evalAst ?(transparent = false) s =
+ wrap_exn transparent (fun () -> self#updateState (state#evalAst s))
end
in
aux
+let choose_selection mmlwidget (element : Gdome.element option) =
+ let rec aux element =
+ if element#hasAttributeNS
+ ~namespaceURI:Misc.helmns
+ ~localName:(Gdome.domString "xref")
+ then
+ mmlwidget#set_selection (Some element)
+ else
+ try
+ match element#get_parentNode with
+ | None -> assert false
+ | Some p -> aux (new Gdome.element_of_node p)
+ with GdomeInit.DOMCastException _ ->
+ debug_print "trying to select above the document root"
+ in
+ match element with
+ | Some x -> aux x
+ | None -> mmlwidget#set_selection None
+
class proof_viewer obj =
object(self)
prerr_endline (gdome_elt#get_nodeName#to_string);
ignore (self#action_toggle gdome_elt)
| 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))
+ ignore (self#connect#selection_changed (choose_selection self))
method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
inherit GMathViewAux.multi_selection_math_view obj
+ initializer
+ ignore (self#connect#selection_changed (choose_selection self))
+
val mutable current_infos = None
method get_selected_terms =
let win metano =
let w =
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
- ~show:true ()
+ ~shadow_type:`IN ~show:true ()
in
let reparent () =
match sequent_viewer#misc#parent with
notebook#append_page ~tab_label:(tab_label metano) (win metano))
metasenv;
switch_page_callback <-
- Some (notebook#connect#after#switch_page ~callback:(fun page ->
+ Some (notebook#connect#switch_page ~callback:(fun page ->
let goal =
try
List.assoc page page2goal
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) ()
+ proof_viewer ~show:true ~packing:gui#proof#scrolledProof#add ()
) in
fun () -> Lazy.force instance
* http://helm.cs.unibo.it/
*)
+open Printf
+
let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR
let is_regular fname = (Unix.stat fname).Unix.st_kind = Unix.S_REG
let is_proof_script fname = true (** TODO Zack *)
let is_proof_object fname = true (** TODO Zack *)
+let append_phrase_sep s =
+ if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
+ s ^ BuildTimeConf.phrase_sep
+ else
+ s
+
(** @return true if file is a (binary) proof object *)
val is_proof_object: string -> bool
+ (** given a phrase, if it doesn't end with BuildTimeConf.phrase_sep, append
+ * it *)
+val append_phrase_sep: string -> string
+
exception No_proof (** no current proof is available *)
exception Cancel
+exception Unbound_identifier of string
(*
let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
* @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
+ * @return success value of the interpretation
*)
- method evalPhrase: ?transparent:bool -> string -> unit
+ method evalPhrase: ?transparent:bool -> string -> bool
+
+ method evalAst: ?transparent:bool -> DisambiguateTypes.tactical -> bool
(** 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
-(*
- (** 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