From 2da9c5cef39f1512fc604adb30e9b0ecae4b2881 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Jan 2003 18:44:20 +0000 Subject: [PATCH] The scratch window is now based on the sequent_viewer widget. --- helm/gTopLevel/gTopLevel.ml | 53 +++++++------- helm/gTopLevel/invokeTactics.ml | 120 +++++++++++-------------------- helm/gTopLevel/invokeTactics.mli | 42 +++++------ 3 files changed, 87 insertions(+), 128 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5b0f3d6e7..c02711dd3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -73,8 +73,6 @@ let postgresqlconnectionstring = let htmlheader_and_content = ref htmlheader;; -let current_scratch_infos = ref None - let check_term = ref (fun _ _ _ -> assert false);; exception RenderingWindowsNotInitialized;; @@ -191,7 +189,7 @@ let check_window outputhtml uris = 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 = @@ -201,11 +199,7 @@ let check_window outputhtml uris = (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 @@ -665,10 +659,8 @@ with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " 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 @@ -1569,12 +1561,12 @@ let new_proof () = 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) ; @@ -2362,18 +2354,28 @@ class scratch_window = 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 = @@ -2815,6 +2817,7 @@ object 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 diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index 0d6f75d99..5e75b5b2d 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -38,29 +38,30 @@ exception RefreshProofException of exn;; 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 ;; @@ -282,41 +283,26 @@ module Make(C:Callbacks) = C.output_html ("

Many terms selected

") - 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 - ("

" ^ Printexc.to_string e ^ "

") - 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 + ("

" ^ Printexc.to_string e ^ "

") + end | [] -> C.output_html ("

No term selected

") @@ -324,42 +310,23 @@ module Make(C:Callbacks) = C.output_html ("

Many terms selected

") - 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 ("

No term selected

") - | 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 @@ -451,15 +418,12 @@ module Make(C:Callbacks) = 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 ;; diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index df911a02f..d527e4faf 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -38,29 +38,30 @@ exception RefreshProofException of exn 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) : @@ -98,16 +99,7 @@ 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 -- 2.39.2