-matitaConsole.cmo: matitaGtkMisc.cmi matitaConsole.cmi
-matitaConsole.cmx: matitaGtkMisc.cmx matitaConsole.cmi
+matitaCicMisc.cmo: matitaTypes.cmo
+matitaCicMisc.cmx: matitaTypes.cmx
+matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaConsole.cmi
+matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaConsole.cmi
matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaGtkMisc.cmi matitaGui.cmi
matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \
matitaGtkMisc.cmx matitaGui.cmi
-matitaInterpreter.cmo: matitaConsole.cmi matitaProof.cmi matitaTypes.cmo \
- matitaInterpreter.cmi
-matitaInterpreter.cmx: matitaConsole.cmx matitaProof.cmx matitaTypes.cmx \
- matitaInterpreter.cmi
-matitaMathView.cmo: matitaTypes.cmo matitaMathView.cmi
-matitaMathView.cmx: matitaTypes.cmx matitaMathView.cmi
+matitaInterpreter.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGui.cmi \
+ matitaMathView.cmi matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi
+matitaInterpreter.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGui.cmx \
+ matitaMathView.cmx matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi
+matitaMathView.cmo: matitaCicMisc.cmo matitaTypes.cmo matitaMathView.cmi
+matitaMathView.cmx: matitaCicMisc.cmx matitaTypes.cmx matitaMathView.cmi
matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \
matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaProof.cmi \
matitaTypes.cmo
matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \
matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaProof.cmx \
matitaTypes.cmx
-matitaProof.cmo: buildTimeConf.cmo matitaTypes.cmo matitaProof.cmi
-matitaProof.cmx: buildTimeConf.cmx matitaTypes.cmx matitaProof.cmi
+matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmo matitaTypes.cmo \
+ matitaProof.cmi
+matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \
+ matitaProof.cmi
matitaTypes.cmo: buildTimeConf.cmo
matitaTypes.cmx: buildTimeConf.cmx
matitaDisambiguator.cmi: matitaTypes.cmo
buildTimeConf.cmo \
matitaGeneratedGui.cmo \
matitaTypes.cmo \
+ matitaCicMisc.cmo \
matitaGtkMisc.cmo \
matitaConsole.cmo \
matitaGui.cmo \
let undo_history_size = 10;;
let console_history_size = 100;;
let gtkrc = "@MATITA_GTKRC@";;
+let base_uri = "cic:/matita";;
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image108">
+ <widget class="GtkImage" id="image116">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image109">
+ <widget class="GtkImage" id="image117">
<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="image110">
+ <widget class="GtkImage" id="image118">
<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="image111">
+ <widget class="GtkImage" id="image119">
<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="image112">
+ <widget class="GtkImage" id="image120">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</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>
</widget>
</widget>
<widget class="GtkWindow" id="CheckWin">
- <property name="title" translatable="yes">Check</property>
+ <property name="width_request">300</property>
+ <property name="height_request">200</property>
+ <property name="title" translatable="yes">Matita: check term</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
<property name="modal">False</property>
<property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<child>
- <placeholder/>
+ <widget class="GtkEventBox" id="CheckWinEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
+
+ <child>
+ <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="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+ </widget>
</child>
</widget>
MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
let sequents_viewer =
+ let set_goal goal =
+ debug_print (sprintf "Setting goal %d" goal);
+ if not (has_proof ()) then assert false;
+ (get_proof ())#set_goal goal
+ in
MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
- ~sequent_viewer ()
+ ~sequent_viewer ~set_goal ()
let new_proof (proof: MatitaTypes.proof) =
let xmldump_observer _ _ = print_endline proof#toString in
- let proof_observer _ (status, (proof_metadata, _)) =
+ let proof_observer _ (status, ()) =
debug_print "proof_observer";
- let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
- ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- proof_metadata
- in
let ((uri_opt, _, _, _), _) = status in
let uri = MatitaTypes.unopt_uri uri_opt in
debug_print "apply transformation";
- let mathml =
- ApplyTransformation.mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
- in
- if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml";
- proof_viewer#load_proof mathml proof_metadata;
+ proof_viewer#load_proof status;
debug_print "/proof_observer"
in
- let sequents_observer _ ((proof, goal_opt), (_, sequents_metadata)) =
+ let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
sequents_viewer#reset;
(match goal_opt with
| None -> ()
| Some goal ->
- sequents_viewer#load_sequents sequents_metadata;
+ sequents_viewer#load_sequents metasenv;
sequents_viewer#goto_sequent goal)
in
ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- sequents_observer);
+ sequents_observer);
ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- proof_observer);
+ proof_observer);
ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
xmldump_observer);
proof#notify;
let proof_handler =
{ MatitaTypes.get_proof = get_proof;
MatitaTypes.abort_proof = abort_proof;
+ MatitaTypes.set_proof = set_proof;
MatitaTypes.has_proof = has_proof;
MatitaTypes.new_proof = new_proof;
MatitaTypes.quit = quit;
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image108 =
+ val image116 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image108" ~info:"GtkImage" xmldata))
- method image108 = image108
+ (Glade.get_widget_msg ~name:"image116" ~info:"GtkImage" xmldata))
+ method image116 = image116
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 image109 =
+ val image117 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image109" ~info:"GtkImage" xmldata))
- method image109 = image109
+ (Glade.get_widget_msg ~name:"image117" ~info:"GtkImage" xmldata))
+ method image117 = image117
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image110 =
+ val image118 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image110" ~info:"GtkImage" xmldata))
- method image110 = image110
+ (Glade.get_widget_msg ~name:"image118" ~info:"GtkImage" xmldata))
+ method image118 = image118
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image111 =
+ val image119 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image111" ~info:"GtkImage" xmldata))
- method image111 = image111
+ (Glade.get_widget_msg ~name:"image119" ~info:"GtkImage" xmldata))
+ method image119 = image119
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 image112 =
+ val image120 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image112" ~info:"GtkImage" xmldata))
- method image112 = image112
+ (Glade.get_widget_msg ~name:"image120" ~info:"GtkImage" xmldata))
+ method image120 = image120
val editMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
new GWindow.window (GtkWindow.Window.cast
(Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
method checkWin = checkWin
+ val checkWinEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"CheckWinEventBox" ~info:"GtkEventBox" xmldata))
+ method checkWinEventBox = checkWinEventBox
+ val scrolledCheck =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"ScrolledCheck" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledCheck = scrolledCheck
+ method reparent parent =
+ checkWinEventBox#misc#reparent parent;
+ toplevel#destroy ()
method check_widgets () = ()
end
val fileMenu_menu : GMenu.menu
val helpMenu : GMenu.menu_item
val helpMenu_menu : GMenu.menu
- val image108 : GMisc.image
- val image109 : GMisc.image
- val image110 : GMisc.image
- val image111 : GMisc.image
- val image112 : GMisc.image
+ val image116 : GMisc.image
+ val image117 : GMisc.image
+ val image118 : GMisc.image
+ val image119 : GMisc.image
+ val image120 : GMisc.image
val mainMenuBar : GMenu.menu_shell
val mainStatusBar : GMisc.statusbar
val mainVPanes : GPack.paned
method fileMenu_menu : GMenu.menu
method helpMenu : GMenu.menu_item
method helpMenu_menu : GMenu.menu
- method image108 : GMisc.image
- method image109 : GMisc.image
- method image110 : GMisc.image
- method image111 : GMisc.image
- method image112 : GMisc.image
+ method image116 : GMisc.image
+ method image117 : GMisc.image
+ method image118 : GMisc.image
+ method image119 : GMisc.image
+ method image120 : GMisc.image
method mainMenuBar : GMenu.menu_shell
method mainStatusBar : GMisc.statusbar
method mainVPanes : GPack.paned
unit ->
object
val checkWin : GWindow.window
+ val checkWinEventBox : GBin.event_box
+ val scrolledCheck : GBin.scrolled_window
val toplevel : GWindow.window
val xml : Glade.glade_xml Gtk.obj
method bind : name:string -> callback:(unit -> unit) -> unit
method checkWin : GWindow.window
+ method checkWinEventBox : GBin.event_box
method check_widgets : unit -> unit
+ method reparent : GObj.widget -> unit
+ method scrolledCheck : GBin.scrolled_window
method toplevel : GWindow.window
method xml : Glade.glade_xml Gtk.obj
end
let proof = new proofWin ~file () in
let check = new checkWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
- [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox ]
+ [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox;
+ check#checkWinEventBox ]
in
let console =
MatitaConsole.console ~evbox:main#consoleEventBox
List.iter (fun (key, callback) -> self#addKeyBinding key callback)
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
+ GdkKeysyms._F4,
+ toggle_win ~check:main#showCheckMenuItem check#checkWin;
];
(* about win *)
ignore (about#aboutWin#event#connect#delete (fun _ -> true));
exception Command_error of string
+let uri name =
+ UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name)
+
let canonical_context metano metasenv =
try
let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
method evalPhrase s = self#evalTactical (self#parsePhrase s)
end
-let check_widget: MatitaTypes.sequents_viewer lazy_t = lazy (
- let gui = MatitaGui.instance () in
- let notebook = GPack.notebook ~show:true ~packing:gui#check#checkWin#add () in
- let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () in
- MatitaMathView.sequents_viewer ~notebook ~sequent_viewer ())
+let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy
+ (let gui = MatitaGui.instance () in
+ MatitaMathView.sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add
+ ())
(** Implements phrases that should be accepted in all states *)
class sharedState
(* do nothing, just for compatibility with coq syntax *)
Some `Command
| TacticAst.Command (TacticAst.Check term) ->
- let dummyno = 1023 in
let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
let (context, metasenv) = get_context_and_metasenv proof_handler in
- let sequent = (dummyno, context, term) in
- let metadata = Cic2acic.asequent_of_sequent metasenv sequent in
+ let dummyno = CicMkImplicit.new_meta metasenv [] in
+ let ty = CicTypeChecker.type_of_aux' metasenv context term in
+ let expr = Cic.Cast (term, ty) in
+ let sequent = (dummyno, context, expr) in
let widget = Lazy.force check_widget in
let gui = MatitaGui.instance () in
gui#check#checkWin#show ();
gui#main#showCheckMenuItem#set_active true;
- widget#reset;
- widget#load_sequents [dummyno, metadata];
- widget#goto_sequent dummyno;
+ widget#load_sequent (sequent::metasenv) dummyno;
None
| tactical ->
raise (Command_error (TacticAstPp.pp_tactical tactical))
method evalTactical = function
| TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
- | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
+ | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) ->
let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
- let proof = MatitaProof.proof ~typ:expr ~metasenv () in
+ let uri =
+ match name_opt with
+ | None -> None
+ | Some name -> Some (uri name)
+ in
+ let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in
proof_handler.MatitaTypes.new_proof proof;
Some `Proof
| TacticAst.Command TacticAst.Quit ->
| TacticAst.Transitivity term ->
EqualityTactics.transitivity_tac (disambiguate term)
| TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
+ | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term)
| TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
| TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
+ | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
+ PrimitiveTactics.elim_intros_simpl_tac (disambiguate term)
| TacticAst.ElimType term ->
EliminationTactics.elim_type_tac (disambiguate term)
| TacticAst.Replace (what, with_what) ->
~with_what:(disambiguate with_what)
(*
(* TODO Zack a lot more of tactics to be implemented here ... *)
- | TacticAst.Absurd
| TacticAst.Change of 'term * 'term * 'ident option
| TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
| TacticAst.Decompose of 'ident * 'ident list
| TacticAst.Discriminate of 'ident
- | TacticAst.Elim of 'term * 'term option
| TacticAst.Fold of reduction_kind * 'term
| TacticAst.Injection of 'ident
| TacticAst.LetIn of 'term * 'ident
| TacticAst.Command (TacticAst.Redo steps) ->
(proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
Some `Proof
+ | TacticAst.Command (TacticAst.Qed name_opt) ->
+ (* TODO Zack this function probably should not simply fail with
+ * Failure, but rather raise some more meaningful exception *)
+ if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
+ let proof = proof_handler.MatitaTypes.get_proof () in
+ (match name_opt with
+ | None -> ()
+ | Some name -> proof#set_uri (uri name));
+ let (uri, metasenv, bo, ty) = proof#proof in
+ let uri = MatitaTypes.unopt_uri uri in
+ if metasenv <> [] then failwith "Proof not completed";
+ let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
+ if not (CicReduction.are_convertible [] proved_ty ty) then
+ failwith "Wrong proof";
+ (* TODO Zack [] probably wrong *)
+ CicEnvironment.add_type_checked_term uri
+ (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+ proof_handler.MatitaTypes.set_proof None;
+ (* TODO Zack a lot more to be done here:
+ * - save object to disk in xml format
+ * - collect metadata
+ * - register uri to the getter *)
+ Some `Command
| TacticAst.Seq tacticals ->
(* TODO Zack check for proof completed at each step? *)
List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
* http://cs.unibo.it/helm/.
*)
-(***************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* 29/01/2003 Claudio Sacerdoti Coen *)
-(* *)
-(* *)
-(***************************************************************************)
-
open Printf
+open MatitaCicMisc
open MatitaTypes
(* List utility functions *)
in
aux
-(* End of the list utility functions *)
+class proof_viewer obj =
+ object(self)
+
+ inherit GMathViewAux.single_selection_math_view obj
+
+(* initializer self#set_log_verbosity 3 *)
+
+ val mutable current_infos = None
+ val mutable current_mathml = None
+
+ method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
+ let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
+ Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+ ids_to_hypotheses);
+ let mathml =
+ ApplyTransformation.mml_of_cic_object ~explode_all:true
+ (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
+ in
+ match current_mathml with
+ | None ->
+ debug_print "no previous MathML";
+ self#load_root ~root:mathml#get_documentElement ;
+ current_mathml <- Some mathml
+ | Some current_mathml ->
+ debug_print "Previous MathML available: xmldiffing ...";
+ self#freeze ;
+ XmlDiff.update_dom ~from:current_mathml mathml ;
+ self#thaw
+ end
class sequent_viewer obj =
object(self)
| None -> assert false (* "ERROR: No current term!!!" *)
) selections
- method load_sequent (mml:Gdome.document)
- (metadata:MatitaTypes.sequents_metadata) sequent_no
- =
+ method load_sequent metasenv metano =
+(*
let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
- ids_to_hypotheses)
- =
- try
- List.assoc sequent_no metadata
- with Not_found -> assert false
+ ids_to_hypotheses) =
+ Cic2acic.asequent_of_sequent metasenv conjecture
+ in
+*)
+ let sequent = CicUtil.lookup_meta metano metasenv in
+ let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses)) =
+ ApplyTransformation.mml_of_cic_sequent metasenv sequent
in
current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
- self#load_root ~root:mml#get_documentElement
+ debug_print "load_sequent: dumping MathML to /tmp/prova";
+ ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ());
+ self#load_root ~root:mathml#get_documentElement
end
-class proof_viewer obj =
- object(self)
-
- inherit GMathViewAux.single_selection_math_view obj
-
-(* initializer self#set_log_verbosity 3 *)
-
- val mutable current_infos = None
- val mutable current_mml = None
-
- method load_proof (mml:Gdome.document) (metadata:MatitaTypes.proof_metadata) =
- let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
- ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- metadata
- in
- current_infos <-
- Some
- (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
- match current_mml with
- | None ->
- MatitaTypes.debug_print "no previous MathML";
- self#load_root ~root:mml#get_documentElement ;
- current_mml <- Some mml
- | Some current_mml' ->
- MatitaTypes.debug_print "Previous MathML available: xmldiffing ...";
- self#freeze ;
- XmlDiff.update_dom ~from:current_mml' mml ;
- self#thaw
- end
class sequents_viewer ~(notebook:GPack.notebook)
- ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
=
object (self)
val mutable pages = 0
val mutable switch_page_callback = None
- val mutable mathmls = []
- val mutable metadata = None
val mutable page2goal = [] (* associative list: page no -> goal no *)
val mutable goal2page = [] (* the other way round *)
+ val mutable _metasenv = []
method reset =
for i = 1 to pages do notebook#remove_page 0 done;
pages <- 0;
- mathmls <- [];
- metadata <- None;
page2goal <- [];
goal2page <- [];
+ _metasenv <- [];
(match switch_page_callback with
| Some id ->
GtkSignal.disconnect notebook#as_widget id;
switch_page_callback <- None
| None -> ())
- method load_sequents (metadata': MatitaTypes.sequents_metadata) =
- metadata <- Some metadata';
- let sequents = metadata' in
- let sequents_no = List.length sequents in
+ method load_sequents metasenv =
+ let sequents_no = List.length metasenv in
+ _metasenv <- metasenv;
debug_print (sprintf "sequents no: %d" sequents_no);
pages <- sequents_no;
let widget = sequent_viewer#coerce in
let page = ref 0 in
List.iter
- (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) ->
+ (fun (metano, _, _) ->
page2goal <- (!page, metano) :: page2goal;
goal2page <- (metano, !page) :: goal2page;
+ incr page;
let tab_label =
(GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
in
- notebook#append_page ~tab_label widget;
- let mathml = lazy
- (let content_sequent = Cic2content.map_sequent asequent in
- let pres_sequent =
- Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
- in
- let xmlpres = Box.document_of_box pres_sequent in
- Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
- in
- mathmls <- (metano, mathml) :: mathmls)
- sequents;
- mathmls <- List.rev mathmls;
+ notebook#append_page ~tab_label widget)
+ metasenv;
switch_page_callback <-
(* TODO Zack the "#after" may probably be removed after Luca's fix for
* widget not loading documents before being realized *)
Some (notebook#connect#after#switch_page ~callback:(fun page ->
debug_print "switch_page callback";
- self#render_page page))
+ let goal =
+ try
+ List.assoc page page2goal
+ with Not_found -> assert false
+ in
+ set_goal goal;
+ self#render_page goal))
+
+ method private render_page goal =
+ sequent_viewer#load_sequent _metasenv goal
method goto_sequent goal =
let page =
with Not_found -> assert false
in
notebook#goto_page page;
- self#render_page page
-
- method private render_page page =
- let metadata =
- match metadata with Some metadata -> metadata | None -> assert false
- in
- let (metano, mathml) = List.nth mathmls page in
- sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
+ self#render_page goal
end
[]
let sequents_viewer ~(notebook:GPack.notebook)
- ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
=
- new sequents_viewer ~notebook ~sequent_viewer ()
+ new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
val sequents_viewer:
notebook:GPack.notebook ->
sequent_viewer:MatitaTypes.sequent_viewer ->
+ set_goal:(int -> unit) ->
unit ->
MatitaTypes.sequents_viewer
* http://helm.cs.unibo.it/
*)
- (** create a Cic.CurrentProof from a given proof *)
-let currentProof (uri, metasenv, bo, ty) =
- let uri = MatitaTypes.unopt_uri uri in
- (* TODO CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+open MatitaCicMisc
+let init_metadata _ = ()
+let compute_metadata _ _ = ()
+
+(*
let init_metadata status =
let ((_, metasenv, _, _) as proof, _) = status in
let proof_object_metadata = (* compute proof annotations *)
- Cic2acic.acic_object_of_cic_object (currentProof proof)
+ Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
in
let sequents_metadata = (* compute all sequent annotations from scratch *)
List.map
(proof_object_metadata, sequents_metadata)
let compute_metadata (old_status, old_metadata) new_status =
- let ((_, new_metasenv, _, _) as new_proof, _) = new_status in
+ let ((_, new_metasenv, _, _) as new_proof, goal_opt) = new_status in
let proof_object_metadata = (* compute proof annotations *)
- Cic2acic.acic_object_of_cic_object (currentProof new_proof)
+ let obj =
+ match goal_opt with
+ | Some _ -> cicCurrentProof new_proof
+ | None -> cicConstant new_proof
+ in
+ Cic2acic.acic_object_of_cic_object obj
in
let sequents_metadata = (* compute all sequent annotations from scratch *)
(** TODO Zack could we reuse some of the annotations from the previous
new_metasenv
in
(proof_object_metadata, sequents_metadata)
+*)
class proof ?uri ~typ ~metasenv ~body () =
object (self)
- inherit [MatitaTypes.hist_metadata]
+ inherit [unit]
StatefulProofEngine.status
~history_size:BuildTimeConf.undo_history_size ?uri ~typ ~body ~metasenv
init_metadata compute_metadata ()
method toXml =
- let currentproof = currentProof self#proof in
+ let currentproof = cicCurrentProof self#proof in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
in
(DisambiguateTypes.environment * Cic.metasenv * Cic.term)
end
+(*
type sequents_metadata =
(int * (** sequent (meta) index *)
(Cic.annconjecture * (** annotated conjecture *)
(Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *)
(Cic.id, Cic.hypothesis) Hashtbl.t (** ids_to_hypotheses *)
type hist_metadata = proof_metadata * sequents_metadata
+*)
class type proof =
object
- inherit [hist_metadata] StatefulProofEngine.status
+ inherit [unit] StatefulProofEngine.status
(** return a pair of "xml" (as defined in Xml module) representing the *
* current proof type and body, respectively *)
type proof_handler =
{ get_proof: unit -> proof; (* return current proof or fail *)
+ set_proof: proof option -> unit;
abort_proof: unit -> unit;(* abort current proof, cleaning up garbage *)
has_proof: unit -> bool; (* check if a current proof is available or not *)
new_proof: proof -> unit; (* as a set_proof but takes care also to register
(** {2 MathML widgets} *)
type mml_of_cic_sequent =
- Cic.metasenv -> int * Cic.context * Cic.term ->
+ Cic.metasenv -> Cic.conjecture ->
Gdome.document *
((Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.id option) Hashtbl.t *
object
inherit GMathViewAux.single_selection_math_view
- method load_proof: Gdome.document -> proof_metadata -> unit
+ method load_proof: StatefulProofEngine.proof_status -> unit
end
class type sequent_viewer =
method get_selected_hypotheses: Cic.hypothesis list
(** load a sequent and render it into parent widget *)
- method load_sequent: Gdome.document -> sequents_metadata -> int -> unit
+ method load_sequent: Cic.metasenv -> int -> unit
end
class type sequents_viewer =
object
method reset: unit
- method load_sequents: sequents_metadata -> unit
+ method load_sequents: Cic.metasenv -> unit
method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
end
projects / helm.git / commitdiff