let href_ds = Gdome.domString "href"
let xref_ds = Gdome.domString "xref"
+(* ids_to_terms should not be passed here, is just for debugging *)
+let find_root_id annobj id ids_to_father_ids ids_to_terms =
+ let find_parent id ids =
+ let rec aux id =
+(* (prerr_endline (sprintf "id %s = %s" id
+ (try
+ CicPp.ppterm (Hashtbl.find ids_to_terms id)
+ with Not_found -> "NONE"))); *)
+ if List.mem id ids then Some id
+ else
+ (match
+ (try Hashtbl.find ids_to_father_ids id with Not_found -> None)
+ with
+ | None -> None
+ | Some id' -> aux id')
+ in
+ aux id
+ in
+ let return_father id ids =
+ match find_parent id ids with
+ | None -> assert false
+ | Some parent_id -> parent_id
+ in
+ let mk_ids terms = List.map CicUtil.id_of_annterm terms in
+ match annobj with
+ | Cic.AConstant (_, _, _, Some bo, ty, _, _)
+ | Cic.AVariable (_, _, Some bo, ty, _, _)
+ | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) ->
+ return_father id (mk_ids [ty; bo])
+ | Cic.AConstant (_, _, _, None, ty, _, _)
+ | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids [ty])
+ | Cic.AInductiveDefinition _ ->
+ assert false (* TODO *)
+
class clickableMathView obj =
let text_width = 80 in
object (self)
val mutable _cic_info = None
method private set_cic_info info = _cic_info <- info
- method private cic_info =
- match _cic_info with
- | Some info -> info
- | None -> assert false
+ method private cic_info = _cic_info
initializer
self#set_font_size !current_font_size;
val mutable selection_changed = false
method private selection_get_cb ctxt ~info ~time =
+(* prerr_endline "selection_get_cb"; *)
(match self#get_selections with
| [] -> ()
| node :: _ -> ctxt#return (self#string_of_node node))
method private selection_clear_cb sel_event =
+(* prerr_endline "selection_clear_cb"; *)
self#remove_selections;
false
method private button_press_cb gdk_button =
+(* prerr_endline "button_press_cb"; *)
let button = GdkEvent.Button.button gdk_button in
if button = left_button then begin
button_press_x <- GdkEvent.Button.x gdk_button;
false
method private popup_contextual_menu time =
+(* prerr_endline "popup_contextual_menu"; *)
match self#string_of_selection with
| None -> ()
| Some s ->
method update_font_size = self#set_font_size !current_font_size
- method private get_term_by_id context id =
- let ids_to_terms, ids_to_hypotheses = self#cic_info in
+ method private get_term_by_id context cic_info id =
+ let ids_to_terms, ids_to_hypotheses, _, _ = cic_info in
try
`Term (Hashtbl.find ids_to_terms id)
with Not_found ->
`Hyp context'
with Not_found -> assert false
+ method private find_obj_conclusion id =
+ match self#cic_info with
+ | None
+ | Some (_, _, _, None) -> assert false
+ | Some (ids_to_terms, _, ids_to_father_ids, Some annobj) ->
+ let id = find_root_id annobj id ids_to_father_ids ids_to_terms in
+ (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
+
method private string_of_node node =
let get_id (node: Gdome.element) =
let xref_attr =
in
xref_attr#to_string
in
+ let id = get_id node in
let script = MatitaScript.instance () in
let metasenv = script#proofMetasenv in
let context = script#proofContext in
- let conclusion = script#proofConclusion in
+ let metasenv, context, conclusion =
+ if script#onGoingProof () then
+ script#proofMetasenv, script#proofContext, script#proofConclusion
+ else
+ [], [],
+ let t = self#find_obj_conclusion id in
+ MatitaLog.debug (CicPp.ppterm t);
+ t
+ in
(* TODO: code for patterns
let conclusion = (MatitaScript.instance ())#proofConclusion in
let conclusion_pattern =
ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
in
*)
- let dummy_goal = ~-1 in
let string_of_cic_sequent cic_sequent =
let acic_sequent, _, _, ids_to_inner_sorts, _ =
Cic2acic.asequent_of_sequent metasenv cic_sequent
let markup = CicNotationPres.render ids_to_uris pped_ast in
BoxPp.render_to_string text_width markup
in
- let term = self#get_term_by_id context (get_id node) in
+ let cic_info =
+ match self#cic_info with Some info -> info | None -> assert false
+ in
let cic_sequent =
- match term with
+ match self#get_term_by_id context cic_info id with
| `Term t ->
let context' =
- match
- ProofEngineHelpers.locate_in_conjecture t
- (dummy_goal, context, conclusion)
- with
+ match
+ ProofEngineHelpers.locate_in_conjecture t
+ (~-1, context, conclusion)
+ with
[context,_] -> context
| _ -> assert false (* since it uses physical equality *)
in
- dummy_goal, context', t
- | `Hyp context -> dummy_goal, context, Cic.Rel 1
+ ~-1, context', t
+ | `Hyp context -> ~-1, context, Cic.Rel 1
in
string_of_cic_sequent cic_sequent
~font_size:None ~log_verbosity:None))
[]
-class sequentViewer obj =
+class cicMathView obj =
object (self)
inherit clickableMathView obj
+ val mutable current_mathml = None
+
method load_sequent metasenv metano =
let sequent = CicUtil.lookup_meta metano metasenv in
- let (mathml, (_, (ids_to_terms, _, ids_to_hypotheses,_ ))) =
+ let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) =
ApplyTransformation.mml_of_cic_sequent metasenv sequent
in
- self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses));
+ self#set_cic_info
+ (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, None));
let name = "sequent_viewer.xml" in
MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
self#load_root ~root:mathml#get_documentElement
- end
-class sequentsViewer ~(notebook:GPack.notebook)
- ~(sequentViewer:sequentViewer) ()
-=
+ method load_object obj =
+ let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
+ let (mathml,
+ (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, _)))
+ =
+ ApplyTransformation.mml_of_cic_object obj
+ in
+ self#set_cic_info
+ (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Some annobj));
+ (match current_mathml with
+ | Some current_mathml when use_diff ->
+ self#freeze;
+ XmlDiff.update_dom ~from:current_mathml mathml;
+ self#thaw
+ | _ ->
+ let name = "cic_browser.xml" in
+ MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+ ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
+ self#load_root ~root:mathml#get_documentElement;
+ current_mathml <- Some mathml);
+end
+
+class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
object (self)
inherit scriptAccessor
val mutable goal2win = [] (* associative list: goal no -> scrolled win *)
val mutable _metasenv = []
val mutable scrolledWin: GBin.scrolled_window option = None
- (* scrolled window to which the sequentViewer is currently attached *)
+ (* scrolled window to which cicMathView is currently attached *)
method private tab_label metano =
(GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
(match scrolledWin with
| Some w ->
(* removing page from the notebook will destroy all contained widget,
- * we do not want the sequentViewer to be destroyed as well *)
- w#remove sequentViewer#coerce;
+ * we do not want the cicMathView to be destroyed as well *)
+ w#remove cicMathView#coerce;
scrolledWin <- None
| None -> ());
for i = 1 to pages do notebook#remove_page 0 done;
in
let reparent () =
scrolledWin <- Some w;
- match sequentViewer#misc#parent with
- | None -> w#add sequentViewer#coerce
+ match cicMathView#misc#parent with
+ | None -> w#add cicMathView#coerce
| Some parent ->
let parent =
- match sequentViewer#misc#parent with
+ match cicMathView#misc#parent with
None -> assert false
| Some p -> GContainer.cast_container p
in
- parent#remove sequentViewer#coerce;
- w#add sequentViewer#coerce
+ parent#remove cicMathView#coerce;
+ w#add cicMathView#coerce
in
goal2win <- (metano, reparent) :: goal2win;
w#coerce
self#render_page ~page ~goal))
method private render_page ~page ~goal =
- sequentViewer#load_sequent _metasenv goal;
+ cicMathView#load_sequent _metasenv goal;
try
List.assoc goal goal2win ();
- sequentViewer#set_selection None
+ cicMathView#set_selection None
with Not_found -> assert false
method goto_sequent goal =
unit ->
'widget
-let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+let cicMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
OgtkMathViewProps.set_params
- (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p))
+ (new cicMathView (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size ~log_verbosity))
[]
activate_combo_query arg query
in
let toplevel = win#toplevel in
- let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
+ let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
let fail message =
MatitaGtkMisc.report_error ~title:"Cic browser" ~message
~parent:toplevel ()
ignore(combo#connect#changed ~callback:start_query);
win#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png");
win#mathOrListNotebook#set_show_tabs false;
-
win#browserForwardButton#misc#set_sensitive false;
win#browserBackButton#misc#set_sensitive false;
ignore (win#browserUri#entry#connect#activate (handle_error' (fun () ->
val mutable current_entry = `About `Blank
val mutable current_infos = None
- val mutable current_mathml = None
val model =
new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
current_entry <- entry
method private _loadObj obj =
- self#_showMath;
- (* this must be _before_ loading the document, since
- * if the widget is not mapped (hidden by the notebook)
- * the document is not rendered *)
- 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, ids_to_inner_sorts, ids_to_inner_types) as info)))
- =
- ApplyTransformation.mml_of_cic_object obj
- in
- current_infos <- Some info;
- (match current_mathml with
- | Some current_mathml when use_diff ->
- mathView#freeze;
- XmlDiff.update_dom ~from:current_mathml mathml;
- mathView#thaw
- | _ ->
- let name = "cic_browser.xml" in
- MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
- ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
- mathView#load_root ~root:mathml#get_documentElement;
- current_mathml <- Some mathml);
+ (* showMath must be done _before_ loading the document, since if the
+ * widget is not mapped (hidden by the notebook) the document is not
+ * rendered *)
+ self#_showMath;
+ mathView#load_object obj
method private _loadTermCic term metasenv =
let context = self#script#proofContext in
end
-let sequentsViewer ~(notebook:GPack.notebook)
- ~(sequentViewer:sequentViewer) ()
-=
- new sequentsViewer ~notebook ~sequentViewer ()
+let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
+ new sequentsViewer ~notebook ~cicMathView ()
let cicBrowser () =
let size = BuildTimeConf.browser_history_size in
let history = new MatitaMisc.browser_history size (`About `Blank) in
aux history
-let default_sequentViewer () = sequentViewer ~show:true ()
-let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
+let default_cicMathView () = cicMathView ~show:true ()
+let cicMathView_instance = MatitaMisc.singleton default_cicMathView
let default_sequentsViewer () =
let gui = get_gui () in
- let sequentViewer = sequentViewer_instance () in
- sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
+ let cicMathView = cicMathView_instance () in
+ sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView ()
let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
let mathViewer () =
let update_font_sizes () =
List.iter (fun b -> b#updateFontSize) !cicBrowsers;
- (sequentViewer_instance ())#update_font_size
+ (cicMathView_instance ())#update_font_size
let get_math_views () =
- ((sequentViewer_instance ()) :> MatitaGuiTypes.clickableMathView)
+ ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView)
:: (List.map (fun b -> b#mathView) !cicBrowsers)
let get_selections () =
projects / helm.git / commitdiff