lazy
(let mmlwidget =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term =
exception NoChoice;;
-let
- interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
- ?(enable_button_for_non_vars=false) ~title ~msg uris
+let interactive_user_uri_choice
+ ~(selection_mode:[ `SINGLE | `MULTIPLE ])
+ ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris
=
let only_constant_choices =
lazy
interactive_user_uri_choice ~selection_mode ?ok
?enable_button_for_non_vars ~title ~msg
let interactive_interpretation_choice = interactive_interpretation_choice
- let input_or_locate_uri = input_or_locate_uri
+ let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
end
;;
~packing:(vbox#pack ~expand:true ~padding:5) () in
let sequent_viewer =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
val mutable term = Cic.Rel 1 (* dummy value *)
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
let _ = proofw_ref <- Some proofw in
let hbox3 =
GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
object(self)
method proofw = (assert false : TermViewer.sequent_viewer)
method content = vbox1
(* MAIN *)
let initialize_everything () =
- let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+ let output =
+ TermViewer.proof_viewer
+ ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
+ ~width:350 ~height:280 ()
+ in
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
rendering_window'#set_auto_disambiguation !auto_disambiguation;