let htmlheader_and_content = ref htmlheader;;
-let current_scratch_infos = ref None
-
let check_term = ref (fun _ _ _ -> assert false);;
exception RenderingWindowsNotInitialized;;
in
lazy
(let mmlwidget =
- GMathViewAux.single_selection_math_view
+ TermViewer.sequent_viewer
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term =
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
try
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- current_scratch_infos := Some scratch_infos ;
- mmlwidget#load_doc ~dom:mml
+ mmlwidget#load_sequent [] (111,[],expr)
with
e ->
output_html outputhtml
module InvokeTacticsCallbacks =
struct
let sequent_viewer () = (rendering_window ())#notebook#proofw
- let term_editor () = ((rendering_window ())#inputt : TermEditor.term_editor)
- let get_current_scratch_infos () = !current_scratch_infos
- let set_current_scratch_infos scratch_infos =
- current_scratch_infos := scratch_infos
+ let term_editor () = (rendering_window ())#inputt
+ let scratch_window () = (rendering_window ())#scratch_window
let refresh_proof () =
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let check_term_in_scratch scratch_window metasenv context expr =
try
let ty = CicTypeChecker.type_of_aux' metasenv context expr in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 (Cic.Cast (expr,ty))
- in
- current_scratch_infos := Some scratch_infos ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
+ let expr = Cic.Cast (expr,ty) in
+ scratch_window#show () ;
+ scratch_window#set_term expr ;
+ scratch_window#set_context context ;
+ scratch_window#set_metasenv metasenv ;
+ scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr)
with
e ->
print_endline ("? " ^ CicPp.ppterm expr) ;
let scrolled_window =
GBin.scrolled_window ~border_width:10
~packing:(vbox#pack ~expand:true ~padding:5) () in
- let mmlwidget =
- GMathViewAux.multi_selection_math_view
+ let sequent_viewer =
+ TermViewer.sequent_viewer
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
- method mmlwidget = mmlwidget
+ val mutable term = Cic.Rel 1 (* dummy value *)
+ val mutable context = ([] : Cic.context) (* dummy value *)
+ val mutable metasenv = ([] : Cic.metasenv) (* dummy value *)
+ method sequent_viewer = sequent_viewer
method show () = window#misc#hide () ; window#show ()
+ method term = term
+ method set_term t = term <- t
+ method context = context
+ method set_context t = context <- t
+ method metasenv = metasenv
+ method set_metasenv t = metasenv <- t
initializer
- ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
+ ignore
+ (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer));
ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
- ignore(whdb#connect#clicked (InvokeTactics'.whd_in_scratch self)) ;
- ignore(reduceb#connect#clicked (InvokeTactics'.reduce_in_scratch self)) ;
- ignore(simplb#connect#clicked (InvokeTactics'.simpl_in_scratch self))
+ ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ;
+ ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ;
+ ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch)
end;;
let open_contextual_menu_for_selected_terms mmlwidget infos =
method outputhtml = outputhtml
method inputt = inputt
method output = (output : TermViewer.proof_viewer)
+ method scratch_window = scratch_window
method notebook = notebook
method show = window#show
initializer
module type Callbacks =
sig
+ (* input widgets *)
val sequent_viewer : unit -> TermViewer.sequent_viewer
val term_editor : unit -> TermEditor.term_editor
- val get_current_scratch_infos :
+ val scratch_window :
unit ->
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option
- val set_current_scratch_infos :
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option -> unit
+ < sequent_viewer: TermViewer.sequent_viewer ;
+ show: unit -> unit ;
+ term: Cic.term ;
+ set_term : Cic.term -> unit ;
+ metasenv: Cic.metasenv ;
+ set_metasenv : Cic.metasenv -> unit ;
+ context: Cic.context ;
+ set_context : Cic.context -> unit >
+ (* output messages *)
+ val output_html : string -> unit
+ (* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
+ (* callbacks for user-tactics interaction *)
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback :
Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
- val output_html : string -> unit
end
;;
C.output_html
("<h1 color=\"red\">Many terms selected</h1>")
- let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+ let call_tactic_with_goal_input_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match C.get_current_scratch_infos () with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let id = xpath in
- let expr = tactic term (Hashtbl.find ids_to_terms id) in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
- end
+ let scratch_window = C.scratch_window () in
+ match scratch_window#sequent_viewer#get_selected_terms with
+ [term] ->
+ begin
+ try
+ let expr = tactic term scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;
+ with
+ e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
| [] ->
C.output_html
("<h1 color=\"red\">No term selected</h1>")
C.output_html
("<h1 color=\"red\">Many terms selected</h1>")
- let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
+ let call_tactic_with_goal_inputs_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
+ let scratch_window = C.scratch_window () in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
+ match scratch_window#sequent_viewer#get_selected_terms with
[] ->
C.output_html
("<h1 color=\"red\">No term selected</h1>")
- | l ->
+ | terms ->
try
- match C.get_current_scratch_infos () with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let term_of_node node =
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- let id = xpath in
- Hashtbl.find ids_to_terms id
- in
- let terms = List.map term_of_node l in
- let expr = tactic terms term in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
+ let expr = tactic terms scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;
with
e ->
C.output_html
call_tactic_with_input
(ProofEngine.decompose
~uris_choice_callback:C.decompose_uris_choice_callback)
- let whd_in_scratch scratch_window =
+ let whd_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
- scratch_window
- let reduce_in_scratch scratch_window =
+ let reduce_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
- scratch_window
- let simpl_in_scratch scratch_window =
+ let simpl_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
- scratch_window
end
;;
module type Callbacks =
sig
+ (* input widgets *)
val sequent_viewer : unit -> TermViewer.sequent_viewer
val term_editor : unit -> TermEditor.term_editor
- val get_current_scratch_infos :
+ val scratch_window :
unit ->
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option
- val set_current_scratch_infos :
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option -> unit
+ < sequent_viewer: TermViewer.sequent_viewer ;
+ show: unit -> unit ;
+ term: Cic.term ;
+ set_term : Cic.term -> unit ;
+ metasenv: Cic.metasenv ;
+ set_metasenv : Cic.metasenv -> unit ;
+ context: Cic.context ;
+ set_context : Cic.context -> unit >
+ (* output messages *)
+ val output_html : string -> unit
+ (* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
+ (* callbacks for user-tactics interaction *)
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback :
Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
- val output_html : string -> unit
end
module Make (C : Callbacks) :
val absurd : unit -> unit
val contradiction : unit -> unit
val decompose : unit -> unit
- val whd_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
- val reduce_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
- val simpl_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
+ val whd_in_scratch : unit -> unit
+ val reduce_in_scratch : unit -> unit
+ val simpl_in_scratch : unit -> unit
end
projects / helm.git / commitdiff