From c65f03d089d758a56914f200659eaa0734e14501 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Feb 2003 17:15:24 +0000 Subject: [PATCH] added HBugs interface module for gTopLevel --- helm/gTopLevel/hbugs.ml | 134 +++++++++++++++++++++++++++++++++++++++ helm/gTopLevel/hbugs.mli | 41 ++++++++++++ 2 files changed, 175 insertions(+) create mode 100644 helm/gTopLevel/hbugs.ml create mode 100644 helm/gTopLevel/hbugs.mli diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml new file mode 100644 index 000000000..0d71d94e0 --- /dev/null +++ b/helm/gTopLevel/hbugs.ml @@ -0,0 +1,134 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Hbugs_types;; +open Printf;; + +let debug_print = + let debug = true in + fun s -> prerr_endline (sprintf "DEBUG: %s" s) +;; + +exception NoProofInProgress;; + +module type HbugsActions = + sig + val enable: unit -> unit + val disable: unit -> unit + val toggle: bool -> unit + + val quit: unit -> unit + + val notify: unit -> unit + end + +module Make (Tactics: InvokeTactics.Tactics) : HbugsActions = + struct + let hbugs_client = ref None + + let quit () = + match !hbugs_client with + | Some c -> c#unregisterFromBroker () + | None -> () + + let hbugs_enabled = ref false + + let get_hbugs_client () = + match !hbugs_client with + | Some c -> c + | None -> assert false + + let disable () = + match !hbugs_client with None -> () | Some c -> c#hide () + + (** send current proof assistant state to hbugs broker *) + let notify () = + try + if !hbugs_enabled then begin + let client = get_hbugs_client () in + let goal = + match !ProofEngine.goal with + | Some g -> g + | None -> raise NoProofInProgress + in + let (type_string, body_string) = + let (type_xml, body_xml) = ProofEngine.get_current_status_as_xml () in + (Xml.pp_to_string type_xml, Xml.pp_to_string body_xml) + in + let new_state = + (Misc.strip_xml_headings type_string, + Misc.strip_xml_headings body_string, + goal) + in + client#stateChange new_state + end + with NoProofInProgress -> () + + let use_hint = function + | Use_ring_Luke -> Tactics.ring () + | Use_fourier_Luke -> Tactics.fourier () + | Use_reflexivity_Luke -> Tactics.reflexivity () + | Use_symmetry_Luke -> Tactics.symmetry () + | Use_assumption_Luke -> Tactics.assumption () + | Use_contradiction_Luke -> Tactics.contradiction () + | Use_exists_Luke -> Tactics.exists () + | Use_split_Luke -> Tactics.split () + | Use_left_Luke -> Tactics.left () + | Use_right_Luke -> Tactics.right () + | Use_apply_Luke term -> Tactics.apply ~term () + | Hints _ -> assert false + + let rec enable () = + (match !hbugs_client with + | None -> (* create an hbugs client and show its window *) + hbugs_client := + (try + Some + (new Hbugs_client.hbugsClient + ~on_use_hint: use_hint + ~on_exit: ignore (* TODO disable hbugs on 'on_exit' callback *) + ()) + with e -> + prerr_endline (sprintf "Can't start HBugs client: %s" + (Printexc.to_string e)); + None); + (match !hbugs_client with + |Some client -> + client#show (); + client#subscribeAll () + | None -> ()) + | Some c -> (* show hbugs client window *) + c#show ()) + + let toggle state = + if state <> !hbugs_enabled then (* status has been changed *) + (if state then enable () else disable ()); + hbugs_enabled := state + + end + diff --git a/helm/gTopLevel/hbugs.mli b/helm/gTopLevel/hbugs.mli new file mode 100644 index 000000000..2982ba09b --- /dev/null +++ b/helm/gTopLevel/hbugs.mli @@ -0,0 +1,41 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module type HbugsActions = + sig + val enable: unit -> unit + val disable: unit -> unit + val toggle: bool -> unit + + val quit: unit -> unit + + val notify: unit -> unit + end + +module Make (Tactics: InvokeTactics.Tactics) : HbugsActions + -- 2.39.2