--- /dev/null
+hbugs_common.cmi: hbugs_types.cmi
+hbugs_id_generator.cmi: hbugs_types.cmi
+hbugs_messages.cmi: hbugs_types.cmi
+hbugs_client.cmi: hbugs_types.cmi
+hbugs_misc.cmo: hbugs_misc.cmi
+hbugs_misc.cmx: hbugs_misc.cmi
+hbugs_common.cmo: hbugs_types.cmi hbugs_common.cmi
+hbugs_common.cmx: hbugs_types.cmi hbugs_common.cmi
+hbugs_id_generator.cmo: hbugs_id_generator.cmi
+hbugs_id_generator.cmx: hbugs_id_generator.cmi
+hbugs_messages.cmo: hbugs_misc.cmi hbugs_types.cmi hbugs_messages.cmi
+hbugs_messages.cmx: hbugs_misc.cmx hbugs_types.cmi hbugs_messages.cmi
+hbugs_client_gui.cmo: hbugs_client_gui.cmi
+hbugs_client_gui.cmx: hbugs_client_gui.cmi
+hbugs_client.cmo: hbugs_client_gui.cmi hbugs_common.cmi \
+ hbugs_id_generator.cmi hbugs_messages.cmi hbugs_misc.cmi hbugs_types.cmi \
+ hbugs_client.cmi
+hbugs_client.cmx: hbugs_client_gui.cmx hbugs_common.cmx \
+ hbugs_id_generator.cmx hbugs_messages.cmx hbugs_misc.cmx hbugs_types.cmi \
+ hbugs_client.cmi
--- /dev/null
+
+# Targets description:
+# all (default) -> builds hbugs bytecode library hbugs.cma
+# opt -> builds hbugs native library hbugs.cmxa
+# daemons -> builds hbugs broker and tutors executables
+#
+# start -> starts up broker and tutors
+# stop -> stop broker and tutors
+#
+# broker -> builds broker executable
+# tutors -> builds tutors executables
+# client -> builds hbugs client
+
+PACKAGE = hbugs
+REQUIRES = \
+ pcre lablgtk2.glade \
+ helm-thread helm-xml helm-pxp helm-tactics
+
+IMPLEMENTATION_FILES = \
+ hbugs_misc.ml \
+ hbugs_common.ml \
+ hbugs_id_generator.ml \
+ hbugs_messages.ml \
+ hbugs_client_gui.ml \
+ hbugs_client.ml
+INTERFACE_FILES = \
+ hbugs_types.mli \
+ $(patsubst %.ml, %.mli, $(IMPLEMENTATION_FILES))
+
+include ../Makefile.common
+include .tutors.ml
+include .generated_tutors.ml
+
+.tutors.ml:
+ echo -n "TUTORS_ML = " > $@
+ scripts/ls_tutors.ml | xargs >> $@
+.generated_tutors.ml:
+ echo -n "GENERATED_TUTORS_ML = " > $@
+ scripts/ls_tutors.ml -auto | xargs >> $@
+
+TUTORS = $(patsubst %.ml, %, $(TUTORS_ML))
+TUTORS_OPT = $(patsubst %, %.opt, $(TUTORS))
+GENERATED_TUTORS = $(patsubst %.ml, %, $(GENERATED_TUTORS_ML))
+
+hbugs_client_gui.ml hbugs_client_gui.mli: hbugs_client_gui.glade
+ lablgladecc2 $< > hbugs_client_gui.ml
+ $(OCAMLC) -i hbugs_client_gui.ml > hbugs_client_gui.mli
+
+clean: clean_mains
+.PHONY: clean_mains
+clean_mains:
+ rm -f $(TUTORS) $(TUTORS_OPT) broker{,.opt} client{,.opt}
+distclean: clean
+ rm -f $(GENERATED_TUTORS_ML) hbugs_client_gui.ml{,i}
+ rm -f .tutors.ml .generated_tutors.ml
+
+MAINS_DEPS = \
+ hbugs_misc.cmo \
+ hbugs_messages.cmo \
+ hbugs_id_generator.cmo
+TUTOR_DEPS = $(MAINS_DEPS) \
+ hbugs_tutors.cmo
+BROKER_DEPS = $(MAINS_DEPS) \
+ hbugs_broker_registry.cmo
+CLIENT_DEPS = $(MAINS_DEPS) \
+ hbugs_client_gui.cmo \
+ hbugs_common.cmo \
+ hbugs_client.cmo
+TUTOR_DEPS_OPT = $(patsubst %.cmo, %.cmx, $(TUTOR_DEPS))
+BROKER_DEPS_OPT = $(patsubst %.cmo, %.cmx, $(BROKER_DEPS))
+CLIENT_DEPS_OPT = $(patsubst %.cmo, %.cmx, $(CLIENT_DEPS))
+$(GENERATED_TUTORS_ML): scripts/build_tutors.ml data/tutors_index.xml data/hbugs_tutor.TPL.ml
+ scripts/build_tutors.ml
+hbugs_tutors.cmo: hbugs_tutors.cmi
+hbugs_broker_registry.cmo: hbugs_broker_registry.cmi
+.PHONY: daemons
+daemons: tutors broker
+.PHONY: tutors
+tutors: all $(TUTORS)
+%_tutor: $(TUTOR_DEPS) %_tutor.ml
+ $(OCAMLC) -linkpkg -o $@ $^
+%_tutor.opt: $(TUTOR_DEPS_OPT) %_tutor.ml
+ $(OCAMLOPT) -linkpkg -o $@ $^
+broker: $(BROKER_DEPS) broker.ml
+ $(OCAMLC) -linkpkg -o $@ $^
+broker.opt: $(BROKER_DEPS_OPT) broker.ml
+ $(OCAMLOPT) -linkpkg -o $@ $^
+client: $(CLIENT_DEPS) client.ml
+ $(OCAMLC) -linkpkg -o $@ $^
+client.opt: $(CLIENT_DEPS_OPT) client.ml
+ $(OCAMLOPT) -linkpkg -o $@ $^
+
+.PHONY: start stop
+start:
+ scripts/brokerctl.sh start
+ scripts/sabba.sh start
+stop:
+ scripts/brokerctl.sh stop
+ scripts/sabba.sh stop
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 = true ;;
+let debug_print s = if debug then prerr_endline s ;;
+Http_common.debug := false;;
+
+let daemon_name = "H-Bugs Broker" ;;
+let default_port = 49081 ;;
+let port_env_var = "HELM_HBUGS_BROKER_PORT" ;;
+let port =
+ try
+ int_of_string (Sys.getenv port_env_var)
+ with
+ | Not_found -> default_port
+ | Failure "int_of_string" ->
+ prerr_endline "Warning: invalid port, reverting to default";
+ default_port
+;;
+let usage_string = "HBugs Broker: usage string not yet written :-(";;
+
+exception Unexpected_msg of message;;
+
+let return_xml_msg body outchan =
+ Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
+;;
+let parse_musing_id = function
+ | Musing_started (_, musing_id) ->
+ prerr_endline ("#### Started musing ID: " ^ musing_id);
+ musing_id
+ | Musing_aborted (_, musing_id) -> musing_id
+ | msg ->
+ prerr_endline (sprintf "Assertion failed, received msg: %s"
+ (Hbugs_messages.string_of_msg msg));
+ assert false
+;;
+
+let do_critical =
+ let mutex = Mutex.create () in
+ fun action ->
+ try
+(* debug_print "Acquiring lock ..."; *)
+ Mutex.lock mutex;
+(* debug_print "Lock Acquired!"; *)
+ let res = Lazy.force action in
+(* debug_print "Releaseing lock ..."; *)
+ Mutex.unlock mutex;
+(* debug_print "Lock released!"; *)
+ res
+ with e -> Mutex.unlock mutex; raise e
+;;
+
+ (* registries *)
+let clients = new Hbugs_broker_registry.clients in
+let tutors = new Hbugs_broker_registry.tutors in
+let musings = new Hbugs_broker_registry.musings in
+let registries =
+ [ (clients :> Hbugs_broker_registry.registry);
+ (tutors :> Hbugs_broker_registry.registry);
+ (musings :> Hbugs_broker_registry.registry) ]
+in
+
+let my_own_id = Hbugs_id_generator.new_broker_id () in
+
+ (* debugging: dump broker internal status, used by '/dump' method *)
+let dump_registries () =
+ assert debug;
+ String.concat "\n" (List.map (fun o -> o#dump) registries)
+in
+
+let handle_msg outchan msg =
+ (* messages from clients *)
+ (match msg with
+
+ | Help ->
+ Hbugs_messages.respond_msg (Usage usage_string) outchan
+ | Register_client (client_id, client_url) -> do_critical (lazy (
+ try
+ clients#register client_id client_url;
+ Hbugs_messages.respond_msg (Client_registered my_own_id) outchan
+ with Hbugs_broker_registry.Client_already_in id ->
+ Hbugs_messages.respond_exc "already_registered" id outchan
+ ))
+ | Unregister_client client_id -> do_critical (lazy (
+ if clients#isAuthenticated client_id then begin
+ clients#unregister client_id;
+ Hbugs_messages.respond_msg (Client_unregistered my_own_id) outchan
+ end else
+ Hbugs_messages.respond_exc "forbidden" client_id outchan
+ ))
+ | List_tutors client_id -> do_critical (lazy (
+ if clients#isAuthenticated client_id then begin
+ Hbugs_messages.respond_msg
+ (Tutor_list (my_own_id, tutors#index))
+ outchan
+ end else
+ Hbugs_messages.respond_exc "forbidden" client_id outchan
+ ))
+ | Subscribe (client_id, tutor_ids) -> do_critical (lazy (
+ if clients#isAuthenticated client_id then begin
+ if List.length tutor_ids <> 0 then begin (* at least one tutor id *)
+ if List.for_all tutors#exists tutor_ids then begin
+ clients#subscribe client_id tutor_ids;
+ Hbugs_messages.respond_msg
+ (Subscribed (my_own_id, tutor_ids)) outchan
+ end else (* required subscription to at least one unexistent tutor *)
+ let missing_tutors =
+ List.filter (fun id -> not (tutors#exists id)) tutor_ids
+ in
+ Hbugs_messages.respond_exc
+ "tutor_not_found" (String.concat " " missing_tutors) outchan
+ end else (* no tutor id specified *)
+ Hbugs_messages.respond_exc "no_tutor_specified" "" outchan
+ end else
+ Hbugs_messages.respond_exc "forbidden" client_id outchan
+ ))
+ | State_change (client_id, new_state) -> do_critical (lazy (
+ if clients#isAuthenticated client_id then begin
+ let active_musings = musings#getByClientId client_id in
+ prerr_endline (sprintf "ACTIVE MUSINGS: %s" (String.concat ", " active_musings));
+ if List.length active_musings = 0 then
+ prerr_endline ("No active musings for client " ^ client_id);
+ prerr_endline "CSC: State change!!!" ;
+ let stop_answers =
+ List.map (* collect Abort_musing message's responses *)
+ (fun id -> (* musing id *)
+ let tutor = snd (musings#getByMusingId id) in
+ Hbugs_messages.submit_req
+ ~url:(tutors#getUrl tutor) (Abort_musing (my_own_id, id)))
+ active_musings
+ in
+ let stopped_musing_ids = List.map parse_musing_id stop_answers in
+ List.iter musings#unregister active_musings;
+ (match new_state with
+ | Some new_state -> (* need to start new musings *)
+ let subscriptions = clients#getSubscription client_id in
+ if List.length subscriptions = 0 then
+ prerr_endline ("No subscriptions for client " ^ client_id);
+ let started_musing_ids =
+ List.map (* register new musings and collect their ids *)
+ (fun tutor_id ->
+ let res =
+ Hbugs_messages.submit_req
+ ~url:(tutors#getUrl tutor_id)
+ (Start_musing (my_own_id, new_state))
+ in
+ let musing_id = parse_musing_id res in
+ musings#register musing_id client_id tutor_id;
+ musing_id)
+ subscriptions
+ in
+ Hbugs_messages.respond_msg
+ (State_accepted (my_own_id, stopped_musing_ids, started_musing_ids))
+ outchan
+ | None -> (* no need to start new musings *)
+ Hbugs_messages.respond_msg
+ (State_accepted (my_own_id, stopped_musing_ids, []))
+ outchan)
+ end else
+ Hbugs_messages.respond_exc "forbidden" client_id outchan
+ ))
+
+ (* messages from tutors *)
+
+ | Register_tutor (tutor_id, tutor_url, hint_type, dsc) -> do_critical (lazy (
+ try
+ tutors#register tutor_id tutor_url hint_type dsc;
+ Hbugs_messages.respond_msg (Tutor_registered my_own_id) outchan
+ with Hbugs_broker_registry.Tutor_already_in id ->
+ Hbugs_messages.respond_exc "already_registered" id outchan
+ ))
+ | Unregister_tutor tutor_id -> do_critical (lazy (
+ if tutors#isAuthenticated tutor_id then begin
+ tutors#unregister tutor_id;
+ Hbugs_messages.respond_msg (Tutor_unregistered my_own_id) outchan
+ end else
+ Hbugs_messages.respond_exc "forbidden" tutor_id outchan
+ ))
+
+ | Musing_completed (tutor_id, musing_id, result) -> do_critical (lazy (
+ if not (tutors#isAuthenticated tutor_id) then begin (* unauthorized *)
+ Hbugs_messages.respond_exc "forbidden" tutor_id outchan;
+ end else if not (musings#isActive musing_id) then begin (* too late *)
+ Hbugs_messages.respond_msg (Too_late (my_own_id, musing_id)) outchan;
+ end else begin (* all is ok: autorhized and on time *)
+ (match result with
+ | Sorry -> ()
+ | Eureka hint ->
+ let client_url =
+ clients#getUrl (fst (musings#getByMusingId musing_id))
+ in
+ let res =
+ Hbugs_messages.submit_req ~url:client_url (Hint (my_own_id, hint))
+ in
+ (match res with
+ | Wow _ -> () (* ok: client is happy with our hint *)
+ | unexpected_msg ->
+ prerr_endline
+ (sprintf
+ "Warning: unexpected msg from client: %s\nExpected was: Wow"
+ (Hbugs_messages.string_of_msg msg))));
+ Hbugs_messages.respond_msg (Thanks (my_own_id, musing_id)) outchan;
+ musings#unregister musing_id
+ end
+ ))
+
+ | msg -> (* unexpected message *)
+ debug_print "Unknown message!";
+ Hbugs_messages.respond_exc
+ "unexpected_msg" (Hbugs_messages.string_of_msg msg) outchan)
+in
+(* (* DEBUGGING wrapper around 'handle_msg' *)
+let handle_msg outchan =
+ if debug then
+ (fun msg -> (* filter handle_msg through a function which dumps input
+ messages *)
+ debug_print (Hbugs_messages.string_of_msg msg);
+ handle_msg outchan msg)
+ else
+ handle_msg outchan
+in
+*)
+
+ (* thread action *)
+let callback (req: Http_types.request) outchan =
+ try
+ debug_print ("Connection from " ^ req#clientAddr);
+ debug_print ("Received request: " ^ req#path);
+ (match req#path with
+ (* TODO write help message *)
+ | "/help" -> return_xml_msg "<help> not yet written </help>" outchan
+ | "/act" ->
+ let msg = Hbugs_messages.msg_of_string req#body in
+ handle_msg outchan msg
+ | "/dump" ->
+ if debug then
+ Http_daemon.respond ~body:(dump_registries ()) outchan
+ else
+ Http_daemon.respond_error ~code:400 outchan
+ | _ -> Http_daemon.respond_error ~code:400 outchan);
+ debug_print "Done!\n"
+ with
+ | Http_types.Param_not_found attr_name ->
+ Hbugs_messages.respond_exc "missing_parameter" attr_name outchan
+ | exc ->
+ Hbugs_messages.respond_exc
+ "uncaught_exception" (Printexc.to_string exc) outchan
+in
+
+ (* thread who cleans up ancient client/tutor/musing registrations *)
+let ragman () =
+ let delay = 3600.0 in (* 1 hour delay *)
+ while true do
+ Thread.delay delay;
+ List.iter (fun o -> o#purge) registries
+ done
+in
+
+ (* start daemon *)
+printf "Listening on port %d ...\n" port;
+flush stdout;
+ignore (Thread.create ragman ());
+Http_daemon.start' ~port ~mode:`Thread callback
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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_common;;
+open Printf;;
+
+let client =
+ new Hbugs_client.hbugsClient
+ ~use_hint_callback:
+ (fun hint ->
+ prerr_endline (sprintf "Using hint: %s" (string_of_hint hint)))
+ ~describe_hint_callback:
+ (fun hint ->
+ prerr_endline (sprintf "Describing hint: %s" (string_of_hint hint)))
+ ()
+in
+client#show ();
+GtkThread.main ()
+
--- /dev/null
+*.environment
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 TutorDescription =
+ struct
+ let addr = "@ADDR@"
+ let port = @PORT@
+ let tactic = @TACTIC@
+ let hint = @HINT@
+ let hint_type = "@HINT_TYPE@"
+ let description = "@DESCRIPTION@"
+ let environment_file = "@ENVIRONMENT_FILE@"
+ end
+;;
+module Tutor = Hbugs_tutors.BuildTutor (TutorDescription) ;;
+Tutor.start () ;;
+
--- /dev/null
+<!--
+ Data used to fill template "hbugs_tutor.TPL.ml"
+
+ @ADDR@ tutor ip address
+ @PORT@ tutor tcp port
+ @TACTIC@ tactic to use (OCaml function, must have type
+ ProofEngineTypes.tactic)
+ @HINT@ hint to be sent to client (content of Hbugs_types.Eureka
+ type constructor, must have type Hbugs_types.hint, see
+ hbugs_types.ml)
+ @HINT_TYPE@ hint type (3rd argument of Hbugs_types.Register_tutor type
+ constructor, must have type Hbugs_types.hint_type)
+ @DESCRIPTION@ human readable tutor description
+ @ENVIRONMENT_FILE@ file from which restore proof checking environment on boot
+
+ "source" attribute corresponding OCaml source file
+
+ INVARIANT: XML element name below are lowercase version of @TAGS@ used in
+ template
+
+ TODO: hint type isn't yet well formalized
+-->
+
+<tutors>
+
+ <!-- DEBUGGING -->
+<!--
+ <tutor source="wait_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50111</port>
+ <tactic>Wait.wait_tac</tactic>
+ <hint>Hbugs_types.Use_ring_Luke</hint>
+ <hint_type>Use Ring Luke</hint_type>
+ <description>WAIT FOREVER tutor</description>
+ <environment_file>wait.environment</environment_file>
+ </tutor>
+-->
+
+ <tutor source="ring_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50001</port>
+ <tactic>Ring.ring_tac</tactic>
+ <hint>Hbugs_types.Use_ring_Luke</hint>
+ <hint_type>Use Ring Luke</hint_type>
+ <description>Ring tutor</description>
+ <environment_file>ring.environment</environment_file>
+ </tutor>
+ <tutor source="fourier_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50002</port>
+ <tactic>FourierR.fourier_tac</tactic>
+ <hint>Hbugs_types.Use_fourier_Luke</hint>
+ <hint_type>Use Fourier Luke</hint_type>
+ <description>Fourier tutor</description>
+ <environment_file>fourier.environment</environment_file>
+ </tutor>
+ <tutor source="reflexivity_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50003</port>
+ <tactic>EqualityTactics.reflexivity_tac</tactic>
+ <hint>Hbugs_types.Use_reflexivity_Luke</hint>
+ <hint_type>Use Reflexivity Luke</hint_type>
+ <description>Reflexivity tutor</description>
+ <environment_file>reflexivity.environment</environment_file>
+ </tutor>
+ <tutor source="symmetry_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50004</port>
+ <tactic>EqualityTactics.symmetry_tac</tactic>
+ <hint>Hbugs_types.Use_symmetry_Luke</hint>
+ <hint_type>Use Symmetry Luke</hint_type>
+ <description>Symmetry tutor</description>
+ <environment_file>symmetry.environment</environment_file>
+ </tutor>
+ <tutor source="assumption_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50005</port>
+ <tactic>VariousTactics.assumption_tac</tactic>
+ <hint>Hbugs_types.Use_assumption_Luke</hint>
+ <hint_type>Use Assumption Luke</hint_type>
+ <description>Assumption tutor</description>
+ <environment_file>assumption.environment</environment_file>
+ </tutor>
+ <tutor source="contradiction_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50006</port>
+ <tactic>NegationTactics.contradiction_tac</tactic>
+ <hint>Hbugs_types.Use_contradiction_Luke</hint>
+ <hint_type>Use Contradiction Luke</hint_type>
+ <description>Contradiction tutor</description>
+ <environment_file>contradiction.environment</environment_file>
+ </tutor>
+ <tutor source="exists_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50007</port>
+ <tactic>IntroductionTactics.exists_tac</tactic>
+ <hint>Hbugs_types.Use_exists_Luke</hint>
+ <hint_type>Use Exists Luke</hint_type>
+ <description>Exists tutor</description>
+ <environment_file>exists.environment</environment_file>
+ </tutor>
+ <tutor source="split_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50008</port>
+ <tactic>IntroductionTactics.split_tac</tactic>
+ <hint>Hbugs_types.Use_split_Luke</hint>
+ <hint_type>Use Split Luke</hint_type>
+ <description>Split tutor</description>
+ <environment_file>split.environment</environment_file>
+ </tutor>
+ <tutor source="left_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50009</port>
+ <tactic>IntroductionTactics.left_tac</tactic>
+ <hint>Hbugs_types.Use_left_Luke</hint>
+ <hint_type>Use Left Luke</hint_type>
+ <description>Left tutor</description>
+ <environment_file>left.environment</environment_file>
+ </tutor>
+ <tutor source="right_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50010</port>
+ <tactic>IntroductionTactics.right_tac</tactic>
+ <hint>Hbugs_types.Use_right_Luke</hint>
+ <hint_type>Use Right Luke</hint_type>
+ <description>Right tutor</description>
+ <environment_file>right.environment</environment_file>
+ </tutor>
+ <tutor source="search_pattern_apply_tutor.ml">
+ <no_auto /> <!-- this imply that settings below are not significant -->
+ <addr>127.0.0.1</addr>
+ <port>50011</port>
+ <tactic>PrimitiveTactics.apply_tac</tactic>
+ <hint>Hbugs_types.Use_apply_Luke</hint>
+ <hint_type>Use Apply Luke (with argument)</hint_type>
+ <description>Search pattern apply tutor</description>
+ <environment_file>search_pattern_apply.environment</environment_file>
+ </tutor>
+</tutors>
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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_misc;;
+open Hbugs_types;;
+open Printf;;
+
+exception Client_already_in of client_id;;
+exception Client_not_found of client_id;;
+exception Musing_already_in of musing_id;;
+exception Musing_not_found of musing_id;;
+exception Tutor_already_in of tutor_id;;
+exception Tutor_not_found of tutor_id;;
+
+class type registry =
+ object
+ method dump: string
+ method purge: unit
+ end
+
+let expire_time = 1800. (* 30 minutes *)
+
+class clients =
+ object (self)
+
+ inherit ThreadSafe.threadSafe
+(*
+ (* <DEBUGGING> *)
+ method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ (* </DEBUGGING> *)
+*)
+
+ val timetable: (client_id, float) Hashtbl.t = Hashtbl.create 17
+ val urls: (client_id, string) Hashtbl.t = Hashtbl.create 17
+ val subscriptions: (client_id, tutor_id list) Hashtbl.t = Hashtbl.create 17
+
+ (** INVARIANT: each client registered has an entry in 'urls' hash table
+ _and_ in 'subscriptions hash table even if it hasn't yet invoked
+ 'subscribe' method *)
+
+ method register id url = self#doWriter (lazy (
+ if Hashtbl.mem urls id then
+ raise (Client_already_in id)
+ else begin
+ Hashtbl.add urls id url;
+ Hashtbl.add subscriptions id [];
+ Hashtbl.add timetable id (Unix.time ())
+ end
+ ))
+ method private remove id =
+ Hashtbl.remove urls id;
+ Hashtbl.remove subscriptions id;
+ Hashtbl.remove timetable id
+ method unregister id = self#doWriter (lazy (
+ if Hashtbl.mem urls id then
+ self#remove id
+ else
+ raise (Client_not_found id)
+ ))
+ method isAuthenticated id = self#doReader (lazy (
+ Hashtbl.mem urls id
+ ))
+ method subscribe client_id tutor_ids = self#doWriter (lazy (
+ if Hashtbl.mem urls client_id then
+ Hashtbl.replace subscriptions client_id tutor_ids
+ else
+ raise (Client_not_found client_id)
+ ))
+ method getUrl id = self#doReader (lazy (
+ if Hashtbl.mem urls id then
+ Hashtbl.find urls id
+ else
+ raise (Client_not_found id)
+ ))
+ method getSubscription id = self#doReader (lazy (
+ if Hashtbl.mem urls id then
+ Hashtbl.find subscriptions id
+ else
+ raise (Client_not_found id)
+ ))
+
+ method dump = self#doReader (lazy (
+ "<clients>\n" ^
+ (Hashtbl.fold
+ (fun id url dump ->
+ (dump ^
+ (sprintf "<client id=\"%s\" url=\"%s\">\n" id url) ^
+ "<subscriptions>\n" ^
+ (String.concat "\n" (* id's subscriptions *)
+ (List.map
+ (fun tutor_id -> sprintf "<tutor id=\"%s\" />\n" tutor_id)
+ (Hashtbl.find subscriptions id))) ^
+ "</subscriptions>\n</client>\n"))
+ urls "") ^
+ "</clients>"
+ ))
+ method purge = self#doWriter (lazy (
+ let now = Unix.time () in
+ Hashtbl.iter
+ (fun id birthday ->
+ if now -. birthday > expire_time then
+ self#remove id)
+ timetable
+ ))
+
+ end
+
+class tutors =
+ object (self)
+
+ inherit ThreadSafe.threadSafe
+(*
+ (* <DEBUGGING> *)
+ method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ (* </DEBUGGING> *)
+*)
+
+ val timetable: (tutor_id, float) Hashtbl.t = Hashtbl.create 17
+ val tbl: (tutor_id, string * hint_type * string) Hashtbl.t =
+ Hashtbl.create 17
+
+ method register id url hint_type dsc = self#doWriter (lazy (
+ if Hashtbl.mem tbl id then
+ raise (Tutor_already_in id)
+ else begin
+ Hashtbl.add tbl id (url, hint_type, dsc);
+ Hashtbl.add timetable id (Unix.time ())
+ end
+ ))
+ method private remove id =
+ Hashtbl.remove tbl id;
+ Hashtbl.remove timetable id
+ method unregister id = self#doWriter (lazy (
+ if Hashtbl.mem tbl id then
+ self#remove id
+ else
+ raise (Tutor_not_found id)
+ ))
+ method isAuthenticated id = self#doReader (lazy (
+ Hashtbl.mem tbl id
+ ))
+ method exists id = self#doReader (lazy (
+ Hashtbl.mem tbl id
+ ))
+ method getTutor id = self#doReader (lazy (
+ if Hashtbl.mem tbl id then
+ Hashtbl.find tbl id
+ else
+ raise (Tutor_not_found id)
+ ))
+ method getUrl id =
+ let (url, _, _) = self#getTutor id in
+ url
+ method getHintType id =
+ let (_, hint_type, _) = self#getTutor id in
+ hint_type
+ method getDescription id =
+ let (_, _, dsc) = self#getTutor id in
+ dsc
+ method index = self#doReader (lazy (
+ Hashtbl.fold
+ (fun id (url, hint_type, dsc) idx -> (id, dsc) :: idx) tbl []
+ ))
+
+ method dump = self#doReader (lazy (
+ "<tutors>\n" ^
+ (Hashtbl.fold
+ (fun id (url, hint_type, dsc) dump ->
+ dump ^
+ (sprintf
+"<tutor id=\"%s\" url=\"%s\">\n<hint_type>%s</hint_type>\n<description>%s</description>\n</tutor>"
+ id url hint_type dsc))
+ tbl "") ^
+ "</tutors>"
+ ))
+ method purge = self#doWriter (lazy (
+ let now = Unix.time () in
+ Hashtbl.iter
+ (fun id birthday ->
+ if now -. birthday > expire_time then
+ self#remove id)
+ timetable
+ ))
+
+ end
+
+class musings =
+ object (self)
+
+ inherit ThreadSafe.threadSafe
+(*
+ (* <DEBUGGING> *)
+ method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+ (* </DEBUGGING> *)
+*)
+
+ val timetable: (musing_id, float) Hashtbl.t = Hashtbl.create 17
+ val musings: (musing_id, client_id * tutor_id) Hashtbl.t = Hashtbl.create 17
+ val clients: (client_id, musing_id list) Hashtbl.t = Hashtbl.create 17
+ val tutors: (tutor_id, musing_id list) Hashtbl.t = Hashtbl.create 17
+
+ (** INVARIANT: each registered musing <musing_id, client_id, tutor_id> has
+ an entry in 'musings' table, an entry in 'clients' (i.e. one of the
+ musings for client_id is musing_id) table, an entry in 'tutors' table
+ (i.e. one of the musings for tutor_id is musing_id) and an entry in
+ 'timetable' table *)
+
+
+ method register musing_id client_id tutor_id = self#doWriter (lazy (
+ if Hashtbl.mem musings musing_id then
+ raise (Musing_already_in musing_id)
+ else begin
+ Hashtbl.add musings musing_id (client_id, tutor_id);
+ (* now add this musing as the first one of musings list for client and
+ tutor *)
+ Hashtbl.replace clients client_id
+ (musing_id ::
+ (try Hashtbl.find clients client_id with Not_found -> []));
+ Hashtbl.replace tutors tutor_id
+ (musing_id ::
+ (try Hashtbl.find tutors tutor_id with Not_found -> []));
+ Hashtbl.add timetable musing_id (Unix.time ())
+ end
+ ))
+ method private remove id =
+ (* ASSUMPTION: this method is invoked under a 'writer' lock *)
+ let (client_id, tutor_id) = self#getByMusingId' id in
+ Hashtbl.remove musings id;
+ (* now remove this musing from the list of musings for client and tutor
+ *)
+ Hashtbl.replace clients client_id
+ (List.filter ((<>) id)
+ (try Hashtbl.find clients client_id with Not_found -> []));
+ Hashtbl.replace tutors tutor_id
+ (List.filter ((<>) id)
+ (try Hashtbl.find tutors tutor_id with Not_found -> []));
+ Hashtbl.remove timetable id
+ method unregister id = self#doWriter (lazy (
+ if Hashtbl.mem musings id then
+ self#remove id
+ ))
+ method private getByMusingId' id =
+ (* ASSUMPTION: this method is invoked under a 'reader' lock *)
+ try
+ Hashtbl.find musings id
+ with Not_found -> raise (Musing_not_found id)
+ method getByMusingId id = self#doReader (lazy (
+ self#getByMusingId' id
+ ))
+ method getByClientId id = self#doReader (lazy (
+ try
+ Hashtbl.find clients id
+ with Not_found -> []
+ ))
+ method getByTutorId id = self#doReader (lazy (
+ try
+ Hashtbl.find tutors id
+ with Not_found -> []
+ ))
+ method isActive id = self#doReader (lazy (
+ Hashtbl.mem musings id
+ ))
+
+ method dump = self#doReader (lazy (
+ "<musings>\n" ^
+ (Hashtbl.fold
+ (fun mid (cid, tid) dump ->
+ dump ^
+ (sprintf "<musing id=\"%s\" client=\"%s\" tutor=\"%s\" />\n"
+ mid cid tid))
+ musings "") ^
+ "</musings>"
+ ))
+ method purge = self#doWriter (lazy (
+ let now = Unix.time () in
+ Hashtbl.iter
+ (fun id birthday ->
+ if now -. birthday > expire_time then
+ self#remove id)
+ timetable
+ ))
+
+ end
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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;;
+
+exception Client_already_in of client_id
+exception Client_not_found of client_id
+exception Musing_already_in of musing_id
+exception Musing_not_found of musing_id
+exception Tutor_already_in of tutor_id
+exception Tutor_not_found of tutor_id
+
+class type registry =
+ object
+ method dump: string
+ method purge: unit
+ end
+
+class clients:
+ object
+ (** 'register client_id client_url' *)
+ method register: client_id -> string -> unit
+ method unregister: client_id -> unit
+ method isAuthenticated: client_id -> bool
+ (** subcribe a client to a set of tutor removing previous subcriptions *)
+ method subscribe: client_id -> tutor_id list -> unit
+ method getUrl: client_id -> string
+ method getSubscription: client_id -> tutor_id list
+
+ method dump: string
+ method purge: unit
+ end
+
+class tutors:
+ object
+ method register: tutor_id -> string -> hint_type -> string -> unit
+ method unregister: tutor_id -> unit
+ method isAuthenticated: tutor_id -> bool
+ method exists: tutor_id -> bool
+ method getTutor: tutor_id -> string * hint_type * string
+ method getUrl: tutor_id -> string
+ method getHintType: tutor_id -> hint_type
+ method getDescription: tutor_id -> string
+ method index: tutor_dsc list
+
+ method dump: string
+ method purge: unit
+ end
+
+class musings:
+ object
+ method register: musing_id -> client_id -> tutor_id -> unit
+ method unregister: musing_id -> unit
+ method getByMusingId: musing_id -> client_id * tutor_id
+ method getByClientId: client_id -> musing_id list
+ method getByTutorId: tutor_id -> musing_id list
+ method isActive: musing_id -> bool
+
+ method dump: string
+ method purge: unit
+ end
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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_common;;
+open Hbugs_types;;
+open Printf;;
+
+exception Invalid_URL of string;;
+
+let do_nothing _ = ();;
+
+module SmartHbugs_client_gui =
+ struct
+ class ['a] oneColumnCList gtree_view ~column_type ~column_title
+ =
+ let obj =
+ ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in
+ let columns = new GTree.column_list in
+ let col = columns#add column_type in
+ let vcol = GTree.view_column ~title:column_title ()
+ ~renderer:(GTree.cell_renderer_text[], ["text",col]) in
+ let store = GTree.list_store columns in
+ object(self)
+ inherit GTree.view obj
+ method clear = store#clear
+ method append (v : 'a) =
+ let row = store#append () in
+ store#set ~row ~column:col v;
+ method column = col
+ initializer
+ self#set_model (Some (store :> GTree.model)) ;
+ ignore (self#append_column vcol)
+ end
+
+ class ['a,'b] twoColumnsCList gtree_view ~column1_type ~column2_type
+ ~column1_title ~column2_title
+ =
+ let obj =
+ ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in
+ let columns = new GTree.column_list in
+ let col1 = columns#add column1_type in
+ let vcol1 = GTree.view_column ~title:column1_title ()
+ ~renderer:(GTree.cell_renderer_text[], ["text",col1]) in
+ let col2 = columns#add column2_type in
+ let vcol2 = GTree.view_column ~title:column2_title ()
+ ~renderer:(GTree.cell_renderer_text[], ["text",col2]) in
+ let store = GTree.list_store columns in
+ object(self)
+ inherit GTree.view obj
+ method clear = store#clear
+ method append (v1 : 'a) (v2 : 'b) =
+ let row = store#append () in
+ store#set ~row ~column:col1 v1;
+ store#set ~row ~column:col2 v2
+ method column1 = col1
+ method column2 = col2
+ initializer
+ self#set_model (Some (store :> GTree.model)) ;
+ ignore (self#append_column vcol1) ;
+ ignore (self#append_column vcol2) ;
+ end
+
+ class subscribeWindow () =
+ object(self)
+ inherit Hbugs_client_gui.subscribeWindow ()
+ val mutable tutorsSmartCList = None
+ method tutorsSmartCList =
+ match tutorsSmartCList with
+ None -> assert false
+ | Some w -> w
+ initializer
+ tutorsSmartCList <-
+ Some
+ (new twoColumnsCList self#tutorsCList
+ ~column1_type:Gobject.Data.string ~column2_type:Gobject.Data.string
+ ~column1_title:"Id" ~column2_title:"Description")
+ end
+
+ class hbugsMainWindow () =
+ object(self)
+ inherit Hbugs_client_gui.hbugsMainWindow ()
+ val mutable subscriptionSmartCList = None
+ val mutable hintsSmartCList = None
+ method subscriptionSmartCList =
+ match subscriptionSmartCList with
+ None -> assert false
+ | Some w -> w
+ method hintsSmartCList =
+ match hintsSmartCList with
+ None -> assert false
+ | Some w -> w
+ initializer
+ subscriptionSmartCList <-
+ Some
+ (new oneColumnCList self#subscriptionCList
+ ~column_type:Gobject.Data.string ~column_title:"Description")
+ initializer
+ hintsSmartCList <-
+ Some
+ (new oneColumnCList self#hintsCList
+ ~column_type:Gobject.Data.string ~column_title:"Description")
+ end
+
+ end
+;;
+
+class hbugsClient
+ ?(use_hint_callback: hint -> unit = do_nothing)
+ ?(describe_hint_callback: hint -> unit = do_nothing)
+ ?(destroy_callback: unit -> unit = do_nothing)
+ ()
+ =
+
+ let http_url_RE = Pcre.regexp "^(http://)?(.*):(\\d+)" in
+ let port_of_http_url url =
+ try
+ let subs = Pcre.extract ~rex:http_url_RE url in
+ int_of_string subs.(3)
+ with e -> raise (Invalid_URL url)
+ in
+
+ object (self)
+
+ val mainWindow = new SmartHbugs_client_gui.hbugsMainWindow ()
+ val subscribeWindow = new SmartHbugs_client_gui.subscribeWindow ()
+ val messageDialog = new Hbugs_client_gui.messageDialog ()
+ val myOwnId = Hbugs_id_generator.new_client_id ()
+ val mutable use_hint_callback = use_hint_callback
+ val mutable myOwnUrl = "localhost:49082"
+ val mutable brokerUrl = "localhost:49081"
+ val mutable brokerId: broker_id option = None
+ (* all available tutors, saved last time a List_tutors message was sent to
+ broker *)
+ val mutable availableTutors: tutor_dsc list = []
+ val mutable statusContext = None
+ val mutable subscribeWindowStatusContext = None
+ val mutable debug = false (* enable/disable debugging buttons *)
+ val mutable hints = [] (* actually available hints *)
+
+ initializer
+ self#initGui;
+ self#startLocalHttpDaemon ();
+ self#testLocalHttpDaemon ();
+ self#testBroker ();
+ self#registerToBroker ();
+ self#reconfigDebuggingButtons
+
+ method show = mainWindow#hbugsMainWindow#show
+ method hide = mainWindow#hbugsMainWindow#misc#hide
+
+ method setUseHintCallback callback =
+ use_hint_callback <- callback
+
+ method private debugButtons =
+ List.map
+ (fun (b: GButton.button) -> new GObj.misc_ops b#as_widget)
+ [ mainWindow#startLocalHttpDaemonButton;
+ mainWindow#testLocalHttpDaemonButton; mainWindow#testBrokerButton ]
+
+ method private initGui =
+
+ (* GUI: main window *)
+
+ (* ignore delete events so that hbugs window is closable only using
+ menu; on destroy (e.g. while quitting gTopLevel) self#quit is invoked
+ *)
+
+ ignore (mainWindow#hbugsMainWindow#event#connect#delete (fun _ -> true));
+ ignore (mainWindow#hbugsMainWindow#event#connect#destroy
+ (fun _ -> self#quit (); false));
+
+ (* GUI main window's menu *)
+ mainWindow#toggleDebuggingMenuItem#set_active debug;
+ ignore (mainWindow#toggleDebuggingMenuItem#connect#toggled
+ self#toggleDebug);
+
+ (* GUI: local HTTP daemon settings *)
+ ignore (mainWindow#clientUrlEntry#connect#changed
+ (fun _ -> myOwnUrl <- mainWindow#clientUrlEntry#text));
+ mainWindow#clientUrlEntry#set_text myOwnUrl;
+ ignore (mainWindow#startLocalHttpDaemonButton#connect#clicked
+ self#startLocalHttpDaemon);
+ ignore (mainWindow#testLocalHttpDaemonButton#connect#clicked
+ self#testLocalHttpDaemon);
+
+ (* GUI: broker choice *)
+ ignore (mainWindow#brokerUrlEntry#connect#changed
+ (fun _ -> brokerUrl <- mainWindow#brokerUrlEntry#text));
+ mainWindow#brokerUrlEntry#set_text brokerUrl;
+ ignore (mainWindow#testBrokerButton#connect#clicked self#testBroker);
+ mainWindow#clientIdLabel#set_text myOwnId;
+
+ (* GUI: client registration *)
+ ignore (mainWindow#registerClientButton#connect#clicked
+ self#registerToBroker);
+
+ (* GUI: subscriptions *)
+ ignore (mainWindow#showSubscriptionWindowButton#connect#clicked
+ (fun () ->
+ self#listTutors ();
+ subscribeWindow#subscribeWindow#show ()));
+
+ let get_selected_row_index () =
+ match mainWindow#hintsCList#selection#get_selected_rows with
+ [path] ->
+ (match GTree.Path.get_indices path with
+ [|n|] -> n
+ | _ -> assert false)
+ | _ -> assert false
+ in
+ (* GUI: hints list *)
+ ignore (
+ let event_ops = new GObj.event_ops mainWindow#hintsCList#as_widget in
+ event_ops#connect#button_press
+ (fun event ->
+ if GdkEvent.get_type event = `TWO_BUTTON_PRESS then
+ use_hint_callback (self#hint (get_selected_row_index ())) ;
+ false));
+
+ ignore (mainWindow#hintsCList#selection#connect#changed
+ (fun () ->
+ describe_hint_callback (self#hint (get_selected_row_index ())))) ;
+
+ (* GUI: main status bar *)
+ let ctxt = mainWindow#mainWindowStatusBar#new_context "0" in
+ statusContext <- Some ctxt;
+ ignore (ctxt#push "Ready");
+
+ (* GUI: subscription window *)
+ subscribeWindow#tutorsCList#selection#set_mode `MULTIPLE;
+ ignore (subscribeWindow#subscribeWindow#event#connect#delete
+ (fun _ -> subscribeWindow#subscribeWindow#misc#hide (); true));
+ ignore (subscribeWindow#listTutorsButton#connect#clicked self#listTutors);
+ ignore (subscribeWindow#subscribeButton#connect#clicked
+ self#subscribeSelected);
+ ignore (subscribeWindow#subscribeAllButton#connect#clicked
+ self#subscribeAll);
+ (subscribeWindow#tutorsCList#get_column 0)#set_visible false;
+ let ctxt = subscribeWindow#subscribeWindowStatusBar#new_context "0" in
+ subscribeWindowStatusContext <- Some ctxt;
+ ignore (ctxt#push "Ready");
+
+ (* GUI: message dialog *)
+ ignore (messageDialog#messageDialog#event#connect#delete
+ (fun _ -> messageDialog#messageDialog#misc#hide (); true));
+ ignore (messageDialog#okDialogButton#connect#clicked
+ (fun _ -> messageDialog#messageDialog#misc#hide ()))
+
+ (* accessory methods *)
+
+ (** pop up a (modal) dialog window showing msg to the user *)
+ method private showDialog msg =
+ messageDialog#dialogLabel#set_text msg;
+ messageDialog#messageDialog#show ()
+ (** use showDialog to display an hbugs message to the user *)
+ method private showMsgInDialog msg =
+ self#showDialog (Hbugs_messages.string_of_msg msg)
+
+ (** create a new thread which sends msg to broker, wait for an answer and
+ invoke callback passing response message as argument *)
+ method private sendReq ?(wait = false) ~msg callback =
+ let thread () =
+ try
+ callback (Hbugs_messages.submit_req ~url:(brokerUrl ^ "/act") msg)
+ with
+ | (Hbugs_messages.Parse_error (subj, reason)) as e ->
+ self#showDialog
+ (sprintf
+"Parse_error, unable to fullfill request. Details follow.
+Request: %s
+Error: %s"
+ (Hbugs_messages.string_of_msg msg) (Printexc.to_string e));
+ | (Unix.Unix_error _) as e ->
+ self#showDialog
+ (sprintf
+"Can't connect to HBugs Broker
+Url: %s
+Error: %s"
+ brokerUrl (Printexc.to_string e))
+ | e ->
+ self#showDialog
+ (sprintf "hbugsClient#sendReq: Uncaught exception: %s"
+ (Printexc.to_string e))
+ in
+ let th = Thread.create thread () in
+ if wait then
+ Thread.join th
+ else ()
+
+ (** check if a broker is authenticated using its broker_id
+ [ Background: during client registration, client save broker_id of its
+ broker, further messages from broker are accepted only if they carry the
+ same broker id ] *)
+ method private isAuthenticated id =
+ match brokerId with
+ | None -> false
+ | Some broker_id -> (id = broker_id)
+
+ (* actions *)
+
+ method private startLocalHttpDaemon =
+ (* flatten an hint tree to an hint list *)
+ let rec flatten_hint = function
+ | Hints hints -> List.concat (List.map flatten_hint hints)
+ | hint -> [hint]
+ in
+ fun () ->
+ let callback req outchan =
+ try
+ (match Hbugs_messages.msg_of_string req#body with
+ | Help ->
+ Hbugs_messages.respond_msg
+ (Usage "Local Http Daemon up and running!") outchan
+ | Hint (broker_id, hint) ->
+ if self#isAuthenticated broker_id then begin
+ let received_hints = flatten_hint hint in
+ List.iter
+ (fun h ->
+ (match h with Hints _ -> assert false | _ -> ());
+ ignore(mainWindow#hintsSmartCList#append(string_of_hint h)))
+ received_hints;
+ hints <- hints @ received_hints;
+ Hbugs_messages.respond_msg (Wow myOwnId) outchan
+ end else (* msg from unauthorized broker *)
+ Hbugs_messages.respond_exc "forbidden" broker_id outchan
+ | msg ->
+ Hbugs_messages.respond_exc
+ "unexpected_msg" (Hbugs_messages.string_of_msg msg) outchan)
+ with (Hbugs_messages.Parse_error _) as e ->
+ Hbugs_messages.respond_exc
+ "parse_error" (Printexc.to_string e) outchan
+ in
+ let addr = "0.0.0.0" in (* TODO actually user specified "My URL" is used
+ only as a value to be sent to broker, local HTTP
+ daemon will listen on "0.0.0.0", port is parsed
+ from My URL though *)
+ let httpDaemonThread () =
+ try
+ Http_daemon.start'
+ ~addr ~port:(port_of_http_url myOwnUrl) ~mode:`Single callback
+ with
+ | Invalid_URL url -> self#showDialog (sprintf "Invalid URL: \"%s\"" url)
+ | e ->
+ self#showDialog (sprintf "Can't start local HTTP daemon: %s"
+ (Printexc.to_string e))
+ in
+ ignore (Thread.create httpDaemonThread ())
+
+ method private testLocalHttpDaemon () =
+ try
+ let msg =
+ Hbugs_misc.http_post ~body:(Hbugs_messages.string_of_msg Help)
+ myOwnUrl
+ in
+ ignore msg
+(* self#showDialog msg *)
+ with
+ | Hbugs_misc.Malformed_URL url ->
+ self#showDialog
+ (sprintf
+ "Handshake with local HTTP daemon failed, Invalid URL: \"%s\""
+ url)
+ | Hbugs_misc.Malformed_HTTP_response res ->
+ self#showDialog
+ (sprintf
+ "Handshake with local HTTP daemon failed, can't parse HTTP response: \"%s\""
+ res)
+ | (Unix.Unix_error _) as e ->
+ self#showDialog
+ (sprintf
+ "Handshake with local HTTP daemon failed, can't connect: \"%s\""
+ (Printexc.to_string e))
+
+ method private testBroker () =
+ self#sendReq ~msg:Help
+ (function
+ | Usage _ -> ()
+ | unexpected_msg ->
+ self#showDialog
+ (sprintf
+ "Handshake with HBugs Broker failed, unexpected message:\n%s"
+ (Hbugs_messages.string_of_msg unexpected_msg)))
+
+ method registerToBroker () =
+ (match brokerId with (* undo previous registration, if any *)
+ | Some id -> self#unregisterFromBroker ()
+ | _ -> ());
+ self#sendReq ~msg:(Register_client (myOwnId, myOwnUrl))
+ (function
+ | Client_registered broker_id -> (brokerId <- Some broker_id)
+ | unexpected_msg ->
+ self#showDialog
+ (sprintf "Client NOT registered, unexpected message:\n%s"
+ (Hbugs_messages.string_of_msg unexpected_msg)))
+
+ method unregisterFromBroker () =
+ self#sendReq ~wait:true ~msg:(Unregister_client myOwnId)
+ (function
+ | Client_unregistered _ -> (brokerId <- None)
+ | unexpected_msg -> ())
+(*
+ self#showDialog
+ (sprintf "Client NOT unregistered, unexpected message:\n%s"
+ (Hbugs_messages.string_of_msg unexpected_msg)))
+*)
+
+ method stateChange new_state =
+ mainWindow#hintsSmartCList#clear ();
+ hints <- [];
+ self#sendReq
+ ~msg:(State_change (myOwnId, new_state))
+ (function
+ | State_accepted _ -> ()
+ | unexpected_msg ->
+ self#showDialog
+ (sprintf "State NOT accepted by Hbugs, unexpected message:\n%s"
+ (Hbugs_messages.string_of_msg unexpected_msg)))
+
+ method hint = List.nth hints
+
+ method private listTutors () =
+ (* wait is set to true just to make sure that after invoking listTutors
+ "availableTutors" is correctly filled *)
+ self#sendReq ~wait:true ~msg:(List_tutors myOwnId)
+ (function
+ | Tutor_list (_, descriptions) ->
+ availableTutors <- (* sort accordingly to tutor description *)
+ List.sort (fun (a,b) (c,d) -> compare (b,a) (d,c)) descriptions;
+ subscribeWindow#tutorsSmartCList#clear ();
+ List.iter
+ (fun (id, dsc) ->
+ ignore (subscribeWindow#tutorsSmartCList#append id dsc))
+ availableTutors
+ | unexpected_msg ->
+ self#showDialog
+ (sprintf "Can't list tutors, unexpected message:\n%s"
+ (Hbugs_messages.string_of_msg unexpected_msg)))
+
+ (* low level used by subscribeSelected and subscribeAll *)
+ method private subscribe' tutors_id =
+ self#sendReq ~msg:(Subscribe (myOwnId, tutors_id))
+ (function
+ | (Subscribed (_, subscribedTutors)) as msg ->
+ let sort = List.sort compare in
+ mainWindow#subscriptionSmartCList#clear ();
+ List.iter
+ (fun tutor_id ->
+ ignore
+ (mainWindow#subscriptionSmartCList#append
+ ( try
+ List.assoc tutor_id availableTutors
+ with Not_found -> assert false )))
+ tutors_id;
+ subscribeWindow#subscribeWindow#misc#hide ();
+ if sort subscribedTutors <> sort tutors_id then
+ self#showDialog
+ (sprintf "Subscription mismatch\n: %s"
+ (Hbugs_messages.string_of_msg msg))
+ | unexpected_msg ->
+ mainWindow#subscriptionSmartCList#clear ();
+ self#showDialog
+ (sprintf "Subscription FAILED, unexpected message:\n%s"
+ (Hbugs_messages.string_of_msg unexpected_msg)))
+
+ method private subscribeSelected () =
+ let tutorsSmartCList = subscribeWindow#tutorsSmartCList in
+ let selectedTutors =
+ List.map
+ (fun p ->
+ tutorsSmartCList#model#get
+ ~row:(tutorsSmartCList#model#get_iter p)
+ ~column:tutorsSmartCList#column1)
+ tutorsSmartCList#selection#get_selected_rows
+ in
+ self#subscribe' selectedTutors
+
+ method subscribeAll () =
+ self#listTutors (); (* this fills 'availableTutors' field *)
+ self#subscribe' (List.map fst availableTutors)
+
+ method private quit () =
+ self#unregisterFromBroker ();
+ destroy_callback ()
+
+ (** enable/disable debugging *)
+ method private setDebug value = debug <- value
+
+ method private reconfigDebuggingButtons =
+ List.iter (* debug value changed, reconfigure buttons *)
+ (fun (b: GObj.misc_ops) -> if debug then b#show () else b#hide ())
+ self#debugButtons;
+
+ method private toggleDebug () =
+ self#setDebug (not debug);
+ self#reconfigDebuggingButtons
+
+ end
+;;
+
--- /dev/null
+
+open Hbugs_types
+
+exception Invalid_URL of string
+
+ (*
+ @param use_hint_callback is called when the user double click on a hint
+ (default: do nothing)
+ @param describe_hint_callback is called when the user click on a hint
+ (default: do nothing)
+ *)
+class hbugsClient :
+ ?use_hint_callback: (hint -> unit) ->
+ ?describe_hint_callback: (hint -> unit) ->
+ ?destroy_callback: (unit -> unit) ->
+ unit ->
+ object
+
+ method show : unit -> unit
+ method hide : unit -> unit
+
+ method setUseHintCallback : (hint -> unit) -> unit
+ method registerToBroker : unit -> unit
+ method unregisterFromBroker : unit -> unit
+ method subscribeAll : unit -> unit
+
+ method stateChange : state option -> unit
+
+ (** @return an hint by index *)
+ method hint : int -> hint
+
+ end
+
--- /dev/null
+<?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
+<!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
+
+<glade-interface>
+<requires lib="gnome"/>
+
+<widget class="GtkWindow" id="hbugsMainWindow">
+ <property name="title" translatable="yes">Hbugs: your personal proof trainer!</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkMenuBar" id="menubar">
+
+ <child>
+ <widget class="GtkMenuItem" id="toolsMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Tools</property>
+ <property name="use_underline">True</property>
+
+ <child>
+ <widget class="GtkMenu" id="toolsMenu_menu">
+ <property name="visible">True</property>
+
+ <child>
+ <widget class="GtkCheckMenuItem" id="toggleDebuggingMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Debugging</property>
+ <property name="use_underline">True</property>
+ <property name="active">False</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox4">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkLabel" id="label11">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">My URL:</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="clientUrlEntry">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Local HTTP daemon URL</property>
+ <property name="can_focus">True</property>
+ <property name="editable">False</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char" translatable="yes">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="startLocalHttpDaemonButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Start the local HTTP daemon listening on the specified URL</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Start!</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="testLocalHttpDaemonButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Test!</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVBox" id="vbox4">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkLabel" id="label1">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Broker:</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="brokerUrlEntry">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">HBugs broker URL</property>
+ <property name="can_focus">True</property>
+ <property name="editable">False</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char" translatable="yes">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="testBrokerButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Test!</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkLabel" id="label2">
+ <property name="label" translatable="yes">Client ID:</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="clientIdLabel">
+ <property name="label" translatable="yes"></property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="registerClientButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">(Re)Register</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVPaned" id="vpaned1">
+ <property name="visible">True</property>
+ <property name="position">0</property>
+
+ <child>
+ <widget class="GtkFrame" id="frame3">
+ <property name="border_width">4</property>
+ <property name="visible">True</property>
+ <property name="label_xalign">0</property>
+ <property name="label_yalign">0.5</property>
+ <property name="shadow_type">GTK_SHADOW_ETCHED_IN</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox6">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow3">
+ <property name="visible">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="subscriptionCList">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">True</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkFixed" id="fixed1">
+ <property name="visible">True</property>
+
+ <child>
+ <widget class="GtkButton" id="showSubscriptionWindowButton">
+ <property name="width_request">0</property>
+ <property name="height_request">0</property>
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Subscribe ...</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="x">0</property>
+ <property name="y">0</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label12">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Subscriptions</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">label_item</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">False</property>
+ <property name="resize">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkFrame" id="frame2">
+ <property name="border_width">4</property>
+ <property name="visible">True</property>
+ <property name="label_xalign">0</property>
+ <property name="label_yalign">0.5</property>
+ <property name="shadow_type">GTK_SHADOW_ETCHED_IN</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox6">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow2">
+ <property name="visible">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="hintsCList">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">True</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label13">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Hints</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">label_item</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkStatusbar" id="mainWindowStatusBar">
+ <property name="has_resize_grip">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="subscribeWindow">
+ <property name="title" translatable="yes">Hbugs: subscribe ...</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox8">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkButton" id="listTutorsButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Refresh</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow4">
+ <property name="visible">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="tutorsCList">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">True</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox5">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkButton" id="subscribeButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Subscribe to Selected</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="subscribeAllButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Subscribe to All</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkStatusbar" id="subscribeWindowStatusBar">
+ <property name="visible">True</property>
+ <property name="has_resize_grip">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="messageDialog">
+ <property name="title" translatable="yes">Message</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">True</property>
+ <property name="default_width">220</property>
+ <property name="default_height">150</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialogVbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialogAction_area1">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="okDialogButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">OK</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">0</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkTable" id="table1">
+ <property name="border_width">5</property>
+ <property name="visible">True</property>
+ <property name="n_rows">1</property>
+ <property name="n_columns">1</property>
+ <property name="homogeneous">False</property>
+ <property name="row_spacing">0</property>
+ <property name="column_spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="dialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes"></property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">True</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="left_attach">0</property>
+ <property name="right_attach">1</property>
+ <property name="top_attach">0</property>
+ <property name="bottom_attach">1</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+</glade-interface>
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 rec string_of_hint = function
+ | Use_ring_Luke -> "Use Ring, Luke!"
+ | Use_fourier_Luke -> "Use Fourier, Luke!"
+ | Use_reflexivity_Luke -> "Use reflexivity, Luke!"
+ | Use_symmetry_Luke -> "Use symmetry, Luke!"
+ | Use_assumption_Luke -> "Use assumption, Luke!"
+ | Use_contradiction_Luke -> "Use contradiction, Luke!"
+ | Use_exists_Luke -> "Use exists, Luke!"
+ | Use_split_Luke -> "Use split, Luke!"
+ | Use_left_Luke -> "Use left, Luke!"
+ | Use_right_Luke -> "Use right, Luke!"
+ | Use_apply_Luke term -> sprintf "Apply %s, Luke!" term
+ | Hints hints -> String.concat "; " (List.map string_of_hint hints)
+;;
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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;;
+
+val string_of_hint: hint -> string
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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/
+ *)
+
+let _ = Random.self_init ()
+
+let id_length = 32
+let min_ascii = 33
+let max_ascii = 126
+ (* characters forbidden inside an XML attribute value. Well, '>' and '''
+ aren't really forbidden, but are listed here ... just to be sure *)
+let forbidden_chars = (* i.e. [ '"'; '&'; '\''; '<'; '>' ] *)
+ [ 34; 38; 39; 60; 62 ] (* assumption: is sorted! *)
+let chars_range = max_ascii - min_ascii + 1 - (List.length forbidden_chars)
+
+ (* return a random id char c such that
+ (min_ascii <= Char.code c) &&
+ (Char.code c <= max_ascii) &&
+ (not (List.mem (Char.code c) forbidden_chars))
+ *)
+let random_id_char () =
+ let rec nth_char ascii shifts = function
+ | [] -> Char.chr (ascii + shifts)
+ | hd::tl when ascii + shifts < hd -> Char.chr (ascii + shifts)
+ | hd::tl (* when ascii + shifts >= hd *) -> nth_char ascii (shifts + 1) tl
+ in
+ nth_char (Random.int chars_range + min_ascii) 0 forbidden_chars
+
+ (* return a random id string which have length id_length *)
+let new_id () =
+ let str = String.create id_length in
+ for i = 0 to id_length - 1 do
+ String.set str i (random_id_char ())
+ done;
+ str
+
+let new_broker_id = new_id
+let new_client_id = new_id
+let new_musing_id = new_id
+let new_tutor_id = new_id
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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;;
+
+val new_broker_id: unit -> broker_id
+val new_client_id: unit -> client_id
+val new_musing_id: unit -> musing_id
+val new_tutor_id: unit -> tutor_id
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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;;
+open Pxp_document;;
+open Pxp_dtd;;
+open Pxp_types;;
+open Pxp_yacc;;
+
+let debug = 2;; (* 0 -> no debug
+ 1 -> waiting for an answer / answer received
+ 2 -> XML messages dumping
+ *)
+
+exception Attribute_not_found of string;;
+exception Empty_node;; (** found a node with no _element_ children *)
+exception No_element_found of string;;
+exception Parse_error of string * string;; (* parsing subject, reason *)
+exception Unexpected_message of message;;
+
+let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
+let get_attr node name =
+ try
+ (match node#attribute name with
+ | Value s -> s
+ | _ -> raise Not_found)
+ with Not_found -> raise (Attribute_not_found name)
+let assert_element n name =
+ match n#node_type with
+ | T_element n when n = name ->
+ ()
+ | _ -> raise (Parse_error ("", "Expected node: " ^ name))
+
+ (** given a string representation of a proof asistant state (e.g. the first
+ child of the XML root of a State_change or Start_musing message), build from
+ it an HBugs view of a proof assistant state *)
+let parse_state (root: ('a node extension as 'a) node) =
+ if (List.filter is_xml_element root#sub_nodes) = [] then
+ raise Empty_node;
+ let buf = Buffer.create 10240 in
+ let node_to_string (node: ('a node extension as 'a) node) =
+ Buffer.clear buf;
+ node#write (`Out_buffer buf) `Enc_utf8;
+ let res = Buffer.contents buf in
+ Buffer.clear buf;
+ res
+ in
+ let (goal_node, type_node, body_node) =
+ try
+ (find_element "CurrentGoal" root,
+ find_element "ConstantType" root,
+ find_element "CurrentProof" root)
+ with Not_found ->
+ raise (Parse_error ("", "Malformed HBugs status XML document"))
+ in
+ assert_element root "gTopLevelStatus";
+ assert_element goal_node "CurrentGoal";
+ assert_element type_node "ConstantType";
+ assert_element body_node "CurrentProof";
+ goal_node#write (`Out_buffer buf) `Enc_utf8;
+ let (type_string, body_string) =
+ (node_to_string type_node, node_to_string body_node)
+ in
+ let goal =
+ try
+ int_of_string (goal_node#data)
+ with Failure "int_of_string" ->
+ raise (Parse_error (goal_node#data, "can't parse goal"))
+ in
+ (type_string, body_string, goal)
+
+ (** parse an hint from an XML node, XML node should have type 'T_element _'
+ (the name is ignored), attributes on it are ignored *)
+let parse_hint node =
+ let rec parse_hint_node node =
+ match node#node_type with
+ | T_element "ring" -> Use_ring_Luke
+ | T_element "fourier" -> Use_fourier_Luke
+ | T_element "reflexivity" -> Use_reflexivity_Luke
+ | T_element "symmetry" -> Use_symmetry_Luke
+ | T_element "assumption" -> Use_assumption_Luke
+ | T_element "contradiction" -> Use_contradiction_Luke
+ | T_element "exists" -> Use_exists_Luke
+ | T_element "split" -> Use_split_Luke
+ | T_element "left" -> Use_left_Luke
+ | T_element "right" -> Use_right_Luke
+ | T_element "apply" -> Use_apply_Luke node#data
+ | T_element "hints" ->
+ Hints
+ (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
+ | _ -> assert false (* CSC: should this assert false be a raise something? *)
+ in
+ match List.filter is_xml_element node#sub_nodes with
+ [node] -> parse_hint_node node
+ | _ -> assert false (* CSC: should this assert false be a raise something? *)
+
+let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
+let parse_tutor_dscs n =
+ List.map
+ (fun n -> (get_attr n "id", n#data))
+ (List.filter is_xml_element n#sub_nodes)
+let parse_tutor_ids node =
+ List.map
+ (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
+
+let tutors_sep = Pcre.regexp ",\\s*"
+
+let pxp_config = PxpHelmConf.pxp_config
+let msg_of_string' s =
+ let root = (* xml tree's root *)
+ parse_wfcontent_entity pxp_config (from_string s) PxpHelmConf.pxp_spec
+ in
+ match root#node_type with
+
+ (* general purpose *)
+ | T_element "help" -> Help
+ | T_element "usage" -> Usage root#data
+ | T_element "exception" -> Exception (get_attr root "name", root#data)
+
+ (* client -> broker *)
+ | T_element "register_client" ->
+ Register_client (get_attr root "id", get_attr root "url")
+ | T_element "unregister_client" -> Unregister_client (get_attr root "id")
+ | T_element "list_tutors" -> List_tutors (get_attr root "id")
+ | T_element "subscribe" ->
+ Subscribe (get_attr root "id", parse_tutor_ids root)
+ | T_element "state_change" ->
+ let state_node =
+ try
+ Some (find_element ~deeply:false "gTopLevelStatus" root)
+ with Not_found -> None
+ in
+ State_change
+ (get_attr root "id",
+ match state_node with
+ | Some n -> (try Some (parse_state n) with Empty_node -> None)
+ | None -> None)
+ | T_element "wow" -> Wow (get_attr root "id")
+
+ (* tutor -> broker *)
+ | T_element "register_tutor" ->
+ let hint_node = find_element "hint_type" root in
+ let dsc_node = find_element "description" root in
+ Register_tutor
+ (get_attr root "id", get_attr root "url",
+ parse_hint_type hint_node, dsc_node#data)
+ | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
+ | T_element "musing_started" ->
+ Musing_started (get_attr root "id", get_attr root "musing_id")
+ | T_element "musing_aborted" ->
+ Musing_started (get_attr root "id", get_attr root "musing_id")
+ | T_element "musing_completed" ->
+ let main_node =
+ try
+ find_element "eureka" root
+ with Not_found -> find_element "sorry" root
+ in
+ Musing_completed
+ (get_attr root "id", get_attr root "musing_id",
+ (match main_node#node_type with
+ | T_element "eureka" ->
+ Eureka (parse_hint main_node)
+ | T_element "sorry" -> Sorry
+ | _ -> assert false)) (* can't be there, see 'find_element' above *)
+
+ (* broker -> client *)
+ | T_element "client_registered" -> Client_registered (get_attr root "id")
+ | T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
+ | T_element "tutor_list" ->
+ Tutor_list (get_attr root "id", parse_tutor_dscs root)
+ | T_element "subscribed" ->
+ Subscribed (get_attr root "id", parse_tutor_ids root)
+ | T_element "state_accepted" ->
+ State_accepted
+ (get_attr root "id",
+ List.map
+ (fun n -> get_attr n "id")
+ (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
+ List.map
+ (fun n -> get_attr n "id")
+ (List.filter is_xml_element (find_element "started" root)#sub_nodes))
+ | T_element "hint" -> Hint (get_attr root "id", parse_hint root)
+
+ (* broker -> tutor *)
+ | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
+ | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
+ | T_element "start_musing" ->
+ let state_node =
+ try
+ find_element ~deeply:false "gTopLevelStatus" root
+ with Not_found -> raise (No_element_found "gTopLevelStatus")
+ in
+ Start_musing (get_attr root "id", parse_state state_node)
+ | T_element "abort_musing" ->
+ Abort_musing (get_attr root "id", get_attr root "musing_id")
+ | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
+ | T_element "too_late" ->
+ Too_late (get_attr root "id", get_attr root "musing_id")
+
+ | _ -> raise (No_element_found s)
+
+let msg_of_string s =
+ try
+ msg_of_string' s
+ with e -> raise (Parse_error (s, Printexc.to_string e))
+
+let pp_state = function
+ | Some (type_string, body_string, goal) ->
+ (* ASSUMPTION: type_string and body_string are well formed XML document
+ contents (i.e. they don't contain heading <?xml ... ?> declaration nor
+ DOCTYPE one *)
+ "<gTopLevelStatus>\n" ^
+ (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
+ type_string ^ "\n" ^
+ body_string ^ "\n" ^
+ "</gTopLevelStatus>\n"
+ | None -> "<gTopLevelStatus />\n"
+
+let rec pp_hint = function
+ | Use_ring_Luke -> sprintf "<ring />"
+ | Use_fourier_Luke -> sprintf "<fourier />"
+ | Use_reflexivity_Luke -> sprintf "<reflexivity />"
+ | Use_symmetry_Luke -> sprintf "<symmetry />"
+ | Use_assumption_Luke -> sprintf "<assumption />"
+ | Use_contradiction_Luke -> sprintf "<contradiction />"
+ | Use_exists_Luke -> sprintf "<exists />"
+ | Use_split_Luke -> sprintf "<split />"
+ | Use_left_Luke -> sprintf "<left />"
+ | Use_right_Luke -> sprintf "<right />"
+ | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
+ | Hints hints ->
+ sprintf "<hints>\n%s\n</hints>"
+ (String.concat "\n" (List.map pp_hint hints))
+
+let pp_hint_type s = s (* TODO pretty print hint_type *)
+let pp_tutor_dscs =
+ List.fold_left
+ (fun s (id, dsc) ->
+ sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
+ ""
+let pp_tutor_ids =
+ List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
+
+let string_of_msg = function
+ | Help -> "<help />"
+ | Usage usage_string -> sprintf "<usage>%s</usage>" usage_string
+ | Exception (name, value) ->
+ sprintf "<exception name=\"%s\">%s</exception>" name value
+ | Register_client (id, url) ->
+ sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
+ | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
+ | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
+ | Subscribe (id, tutor_ids) ->
+ sprintf "<subscribe id=\"%s\">%s</subscribe>"
+ id (pp_tutor_ids tutor_ids)
+ | State_change (id, state) ->
+ sprintf "<state_change id=\"%s\">%s</state_change>"
+ id (pp_state state)
+ | Wow id -> sprintf "<wow id=\"%s\" />" id
+ | Register_tutor (id, url, hint_type, dsc) ->
+ sprintf
+"<register_tutor id=\"%s\" url=\"%s\">
+<hint_type>%s</hint_type>
+<description>%s</description>
+</register_tutor>"
+ id url (pp_hint_type hint_type) dsc
+ | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
+ | Musing_started (id, musing_id) ->
+ sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Musing_aborted (id, musing_id) ->
+ sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Musing_completed (id, musing_id, result) ->
+ sprintf
+ "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
+ id musing_id
+ (match result with
+ | Sorry -> "<sorry />"
+ | Eureka hint -> sprintf "<eureka>%s</eureka>" (pp_hint hint))
+ | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
+ | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
+ | Tutor_list (id, tutor_dscs) ->
+ sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
+ id (pp_tutor_dscs tutor_dscs)
+ | Subscribed (id, tutor_ids) ->
+ sprintf "<subscribed id=\"%s\">%s</subscribed>"
+ id (pp_tutor_ids tutor_ids)
+ | State_accepted (id, stop_ids, start_ids) ->
+ sprintf
+"<state_accepted id=\"%s\">
+<stopped>%s</stopped>
+<started>%s</started>
+</state_accepted>"
+ id
+ (String.concat ""
+ (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
+ (String.concat ""
+ (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
+ | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
+ | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
+ | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
+ | Start_musing (id, state) ->
+ sprintf "<start_musing id=\"%s\">%s</start_musing>"
+ id (pp_state (Some state))
+ | Abort_musing (id, musing_id) ->
+ sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Thanks (id, musing_id) ->
+ sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Too_late (id, musing_id) ->
+ sprintf "<too_late id=\"%s\" musing_id=\"%s\" />" id musing_id
+;;
+
+ (* debugging function that dump on stderr the sent messages *)
+let dump_msg msg =
+ if debug >= 2 then
+ prerr_endline
+ (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
+ (match msg with
+ | State_change _ -> "<state_change>omissis ...</state_change>"
+ | msg -> string_of_msg msg))
+;;
+
+let submit_req ~url msg =
+ dump_msg msg;
+ if debug >= 1 then (prerr_string "Waiting for an answer ... "; flush stderr);
+ let res =
+ msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
+ in
+ if debug >= 1 then (prerr_string "answer received!\n"; flush stderr);
+ res
+;;
+let return_xml_msg body outchan =
+ Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
+;;
+let respond_msg msg outchan =
+ dump_msg msg;
+ return_xml_msg (string_of_msg msg) outchan
+(* close_out outchan *)
+;;
+let respond_exc name value = respond_msg (Exception (name, value));;
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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;;
+
+exception Parse_error of string * string (* parsing subject, reason *)
+exception Unexpected_message of message;;
+
+val msg_of_string: string -> message
+val string_of_msg: message -> string
+
+val submit_req: url:string -> message -> message
+ (** close outchan afterwards *)
+val respond_msg: message -> out_channel -> unit
+ (** close outchan afterwards *)
+ (* exception_name, exception_value, output_channel *)
+val respond_exc: string -> string -> out_channel -> unit
+
+(* TODO the below functions are for debugging only and shouldn't be exposed *)
+val parse_state:
+ ('a Pxp_document.node Pxp_document.extension as 'a) Pxp_document.node ->
+ (string * string * int)
+val pp_state: (string * string * int) option -> string
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 Printf;;
+
+let rec hashtbl_remove_all tbl key =
+ if Hashtbl.mem tbl key then begin
+ Hashtbl.remove tbl key;
+ hashtbl_remove_all tbl key
+ end else
+ ()
+
+ (** follows cut and paste from zack's Http_client_smart module *)
+
+exception Malformed_URL of string;;
+exception Malformed_HTTP_response of string;;
+
+let bufsiz = 16384;;
+let tcp_bufsiz = 4096;;
+
+let body_sep_RE = Pcre.regexp "\r\n\r\n";;
+let http_scheme_RE = Pcre.regexp ~flags:[`CASELESS] "^http://";;
+let url_RE = Pcre.regexp "^([\\w.]+)(:(\\d+))?(/.*)?$";;
+let parse_url url =
+ try
+ let subs =
+ Pcre.extract ~rex:url_RE (Pcre.replace ~rex:http_scheme_RE url)
+ in
+ (subs.(1),
+ (if subs.(2) = "" then 80 else int_of_string subs.(3)),
+ (if subs.(4) = "" then "/" else subs.(4)))
+ with exc -> raise (Malformed_URL url)
+;;
+let get_body answer =
+ match Pcre.split ~rex:body_sep_RE answer with
+ | [_; body] -> body
+ | _ -> raise (Malformed_HTTP_response answer)
+;;
+
+let init_socket addr port =
+ let inet_addr = (Unix.gethostbyname addr).Unix.h_addr_list.(0) in
+ let sockaddr = Unix.ADDR_INET (inet_addr, port) in
+ let suck = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in
+ Unix.connect suck sockaddr;
+ let outchan = Unix.out_channel_of_descr suck in
+ let inchan = Unix.in_channel_of_descr suck in
+ (inchan, outchan)
+;;
+let rec retrieve inchan buf =
+ Buffer.add_string buf (input_line inchan ^ "\n");
+ retrieve inchan buf
+;;
+
+let http_get_iter_buf ~callback url =
+ let (address, port, path) = parse_url url in
+ let buf = String.create tcp_bufsiz in
+ let (inchan, outchan) = init_socket address port in
+ output_string outchan (sprintf "GET %s\r\n" path);
+ flush outchan;
+ (try
+ while true do
+ match input inchan buf 0 tcp_bufsiz with
+ | 0 -> raise End_of_file
+ | bytes when bytes = tcp_bufsiz -> (* buffer full, no need to slice it *)
+ callback buf
+ | bytes when bytes < tcp_bufsiz -> (* buffer not full, slice it *)
+ callback (String.sub buf 0 bytes)
+ | _ -> (* ( bytes < 0 ) || ( bytes > tcp_bufsiz ) *)
+ assert false
+ done
+ with End_of_file -> ());
+ close_in inchan (* close also outchan, same fd *)
+;;
+
+let http_get url =
+ let buf = Buffer.create (tcp_bufsiz * 10) in
+ http_get_iter_buf (fun data -> Buffer.add_string buf data) url;
+ get_body (Buffer.contents buf)
+;;
+
+let http_post ?(body = "") url =
+ let (address, port, path) = parse_url url in
+ let (inchan, outchan) = init_socket address port in
+ output_string outchan (sprintf "POST %s HTTP/1.0\r\n" path);
+ output_string outchan (sprintf "Content-Length: %d\r\n" (String.length body));
+ output_string outchan "\r\n";
+ output_string outchan body;
+ flush outchan;
+ let buf = Buffer.create bufsiz in
+ (try
+ retrieve inchan buf
+ with End_of_file -> close_in inchan); (* close also outchan, same fd *)
+ get_body (Buffer.contents buf)
+;;
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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/
+ *)
+
+ (** helpers *)
+
+ (** remove all bindings of a given key from an hash table *)
+val hashtbl_remove_all: ('a, 'b) Hashtbl.t -> 'a -> unit
+
+ (** follows cut and paste from zack's Http_client_smart module *)
+
+ (** can't parse an HTTP url *)
+exception Malformed_URL of string
+ (** can't parse an HTTP response *)
+exception Malformed_HTTP_response of string
+
+ (** HTTP GET request for a given url, return http response's body *)
+val http_get: string -> string
+ (** HTTP POST request for a given url, return http response's body,
+ body argument, if specified, is sent as body along with request *)
+val http_post: ?body:string -> string -> string
+
+ (** perform an HTTP GET request and apply a given function on each
+ 'slice' of HTTP response read from server *)
+val http_get_iter_buf: callback:(string -> unit) -> string -> unit
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 broker_url = "localhost:49081/act";;
+let dump_environment_on_exit = false;;
+
+let init_tutor = Hbugs_id_generator.new_tutor_id;;
+
+ (** register a tutor to broker *)
+let register_to_broker id url hint_type dsc =
+ try
+ let res =
+ Hbugs_messages.submit_req
+ ~url:broker_url (Register_tutor (id, url, hint_type, dsc))
+ in
+ (match res with
+ | Tutor_registered id ->
+ prerr_endline (sprintf "Tutor registered, broker id: %s" id);
+ id
+ | unexpected_msg ->
+ raise (Hbugs_messages.Unexpected_message unexpected_msg))
+ with e ->
+ failwith (sprintf "Can't register tutor to broker: uncaught exception: %s"
+ (Printexc.to_string e))
+;;
+ (** unregister a tutor from the broker *)
+let unregister_from_broker id =
+ let res = Hbugs_messages.submit_req ~url:broker_url (Unregister_tutor id) in
+ match res with
+ | Tutor_unregistered _ -> prerr_endline "Tutor unregistered!"
+ | unexpected_msg ->
+ failwith
+ (sprintf "Can't unregister from broker, received unexpected msg: %s"
+ (Hbugs_messages.string_of_msg unexpected_msg))
+;;
+
+ (* typecheck a loaded proof *)
+ (* TODO this is a cut and paste from gTopLevel.ml *)
+let typecheck_loaded_proof metasenv bo ty =
+ let module T = CicTypeChecker in
+ ignore (
+ List.fold_left
+ (fun metasenv ((_,context,ty) as conj) ->
+ ignore (T.type_of_aux' metasenv context ty) ;
+ metasenv @ [conj]
+ ) [] metasenv) ;
+ ignore (T.type_of_aux' metasenv [] ty) ;
+ ignore (T.type_of_aux' metasenv [] bo)
+;;
+
+type xml_kind = Body | Type;;
+let mk_dtdname ~ask_dtd_to_the_getter dtd =
+ if ask_dtd_to_the_getter then
+ Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
+ else
+ "http://mowgli.cs.unibo.it/dtd/" ^ dtd
+;;
+ (** this function must be the inverse function of GTopLevel.strip_xml_headings
+ *)
+let add_xml_headings ~kind s =
+ let dtdname = mk_dtdname ~ask_dtd_to_the_getter:true "cic.dtd" in
+ let root =
+ match kind with
+ | Body -> "CurrentProof"
+ | Type -> "ConstantType"
+ in
+ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ^
+ "<!DOCTYPE " ^ root ^ " SYSTEM \""^ dtdname ^ "\">\n\n" ^
+ s
+;;
+
+let load_state (type_string, body_string, goal) =
+ prerr_endline "a0";
+ let ((tmp1, oc1), (tmp2, oc2)) =
+ (Filename.open_temp_file "" "", Filename.open_temp_file "" "")
+ in
+ prerr_endline "a1";
+ output_string oc1 (add_xml_headings ~kind:Type type_string);
+ output_string oc2 (add_xml_headings ~kind:Body body_string);
+ close_out oc1; close_out oc2;
+ prerr_endline (sprintf "Proof Type available in %s" tmp1);
+ prerr_endline (sprintf "Proof Body available in %s" tmp2);
+ let (proof, goal) =
+ prerr_endline "a2";
+ (match CicParser.obj_of_xml tmp1 (Some tmp2) with
+ | Cic.CurrentProof (_,metasenv,bo,ty,_) -> (* TODO il primo argomento e' una URI valida o e' casuale? *)
+ prerr_endline "a3";
+ let uri = UriManager.uri_of_string "cic:/foo.con" in
+ prerr_endline "a4";
+ typecheck_loaded_proof metasenv bo ty;
+ prerr_endline "a5";
+ ((uri, metasenv, bo, ty), goal)
+ | _ -> assert false)
+ in
+ prerr_endline "a6";
+ Sys.remove tmp1; Sys.remove tmp2;
+ (proof, goal)
+
+(* tutors creation stuff from now on *)
+
+module type HbugsTutor =
+ sig
+ val start: unit -> unit
+ end
+
+module type HbugsTutorDescription =
+ sig
+ val addr: string
+ val port: int
+ val tactic: ProofEngineTypes.tactic
+ val hint: hint
+ val hint_type: hint_type
+ val description: string
+ val environment_file: string
+ end
+
+module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
+ struct
+ let broker_id = ref None
+ let my_own_id = init_tutor ()
+ let my_own_addr, my_own_port = Dsc.addr, Dsc.port
+ let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
+
+ let is_authenticated id =
+ match !broker_id with
+ | None -> false
+ | Some broker_id -> id = broker_id
+
+ (* thread who do the dirty work *)
+ let slave (state, musing_id) =
+ prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
+ let (proof, goal) = load_state state in
+ let success =
+ try
+ ignore (Dsc.tactic (proof, goal));
+ true
+ with e -> false
+ in
+ let answer =
+ Musing_completed
+ (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry))
+ in
+ ignore (Hbugs_messages.submit_req ~url:broker_url answer);
+ prerr_endline
+ (sprintf "Bye, I've completed my duties (success = %b)" success)
+
+ let hbugs_callback =
+ (* hashtbl mapping musings ids to PID of threads doing the related (dirty)
+ work *)
+ let slaves = Hashtbl.create 17 in
+ let forbidden () =
+ prerr_endline "ignoring request from unauthorized broker";
+ Exception ("forbidden", "")
+ in
+ function (* _the_ callback *)
+ | Start_musing (broker_id, state) ->
+ if is_authenticated broker_id then begin
+ prerr_endline "received Start_musing";
+ let new_musing_id = Hbugs_id_generator.new_musing_id () in
+ prerr_endline
+ (sprintf "starting a new musing (id = %s)" new_musing_id);
+(* let slave_thread = Thread.create slave (state, new_musing_id) in *)
+ let slave_thread =
+ ExtThread.create slave (state, new_musing_id)
+ in
+ Hashtbl.add slaves new_musing_id slave_thread;
+ Musing_started (my_own_id, new_musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | Abort_musing (broker_id, musing_id) ->
+ if is_authenticated broker_id then begin
+ (try (* kill thread responsible for "musing_id" *)
+ let slave_thread = Hashtbl.find slaves musing_id in
+ ExtThread.kill slave_thread;
+ Hashtbl.remove slaves musing_id
+ with
+ | ExtThread.Can_t_kill (_, reason) ->
+ prerr_endline (sprintf "Unable to kill slave: %s" reason)
+ | Not_found ->
+ prerr_endline (sprintf
+ "Can't find slave corresponding to musing %s, can't kill it"
+ musing_id));
+ Musing_aborted (my_own_id, musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | unexpected_msg ->
+ Exception ("unexpected_msg",
+ Hbugs_messages.string_of_msg unexpected_msg)
+
+ let callback (req: Http_types.request) outchan =
+ try
+ let req_msg = Hbugs_messages.msg_of_string req#body in
+ let answer = hbugs_callback req_msg in
+ Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
+ with Hbugs_messages.Parse_error (subj, reason) ->
+ Http_daemon.respond
+ ~body:(Hbugs_messages.string_of_msg
+ (Exception ("parse_error", reason)))
+ outchan
+
+ let restore_environment () =
+ let ic = open_in Dsc.environment_file in
+ prerr_endline "Restoring environment ...";
+ CicEnvironment.restore_from_channel
+ ~callback:(fun uri -> prerr_endline uri) ic;
+ prerr_endline "... done!";
+ close_in ic
+
+ let dump_environment () =
+ let oc = open_out Dsc.environment_file in
+ prerr_endline "Dumping environment ...";
+ CicEnvironment.dump_to_channel
+ ~callback:(fun uri -> prerr_endline uri) oc;
+ prerr_endline "... done!";
+ close_out oc
+
+ let main () =
+ try
+ Sys.catch_break true;
+ at_exit (fun () ->
+ if dump_environment_on_exit then
+ dump_environment ();
+ unregister_from_broker my_own_id);
+ broker_id :=
+ Some (register_to_broker
+ my_own_id my_own_url Dsc.hint_type Dsc.description);
+ if Sys.file_exists Dsc.environment_file then
+ restore_environment ();
+ Http_daemon.start'
+ ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
+ with Sys.Break -> () (* exit nicely, invoking at_exit functions *)
+
+ let start = main
+
+ end
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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;;
+
+val broker_url: string
+
+val register_to_broker:
+ tutor_id -> string -> hint_type -> string ->
+ broker_id
+val unregister_from_broker: tutor_id -> unit
+
+val init_tutor: unit -> tutor_id
+val load_state:
+ Hbugs_types.state ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal
+
+module type HbugsTutor =
+ sig
+ val start: unit -> unit
+ end
+
+module type HbugsTutorDescription =
+ sig
+ val addr: string
+ val port: int
+ val tactic: ProofEngineTypes.tactic
+ val hint: hint
+ val hint_type: hint_type
+ val description: string
+ val environment_file: string
+ end
+
+module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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/
+ *)
+
+type broker_id = string
+type client_id = string
+type musing_id = string
+type tutor_id = string
+type tutor_dsc = tutor_id * string (* tutor id, tutor description *)
+
+type state = (* proof assitant's state: proof type, proof body, goal *)
+ string * string * int
+
+type hint =
+ (* tactics usage related hints *)
+ | Use_ring_Luke
+ | Use_fourier_Luke
+ | Use_reflexivity_Luke
+ | Use_symmetry_Luke
+ | Use_assumption_Luke
+ | Use_contradiction_Luke
+ | Use_exists_Luke
+ | Use_split_Luke
+ | Use_left_Luke
+ | Use_right_Luke
+ | Use_apply_Luke of string (* use apply tactic on embedded term *)
+ (* hints list *)
+ | Hints of hint list
+
+type hint_type = string (* TODO tipo di consiglio per l'utente *)
+
+type musing_result =
+ | Eureka of hint (* extra information, if any, parsed depending
+ on tutor's hint_type *)
+ | Sorry
+
+ (* for each message, first component is an ID that identify the sender *)
+type message =
+
+ (* general purpose *)
+ | Help (* help request *)
+ | Usage of string (* help response *) (* usage string *)
+ | Exception of string * string (* name, value *)
+
+ (* client -> broker *)
+ | Register_client of client_id * string (* client id, client url *)
+ | Unregister_client of client_id (* client id *)
+ | List_tutors of client_id (* client_id *)
+ | Subscribe of client_id * tutor_id list (* client id, tutor id list *)
+ | State_change of client_id * state option (* client_id, new state *)
+ | Wow of client_id (* client_id *)
+
+ (* tutor -> broker *)
+ | Register_tutor of tutor_id * string * hint_type * string
+ (* tutor id, tutor url, hint type,
+ tutor description *)
+ | Unregister_tutor of tutor_id (* tutor id *)
+ | Musing_started of tutor_id * musing_id (* tutor id, musing id *)
+ | Musing_aborted of tutor_id * musing_id (* tutor id, musing id *)
+ | Musing_completed of tutor_id * musing_id * musing_result
+ (* tutor id, musing id, result *)
+
+ (* broker -> client *)
+ | Client_registered of broker_id (* broker id *)
+ | Client_unregistered of broker_id (* broker id *)
+ | Tutor_list of broker_id * tutor_dsc list (* broker id, tutor list *)
+ | Subscribed of broker_id * tutor_id list (* broker id, tutor list *)
+ | State_accepted of broker_id * musing_id list * musing_id list
+ (* broker id, stopped musing ids,
+ started musing ids *)
+ | Hint of broker_id * hint (* broker id, hint *)
+
+ (* broker -> tutor *)
+ | Tutor_registered of broker_id (* broker id *)
+ | Tutor_unregistered of broker_id (* broker id *)
+ | Start_musing of broker_id * state (* broker id, state *)
+ | Abort_musing of broker_id * musing_id (* broker id, musing id *)
+ | Thanks of broker_id * musing_id (* broker id, musing id *)
+ | Too_late of broker_id * musing_id (* broker id, musing id *)
+
--- /dev/null
+#!/bin/sh
+daemon="broker"
+if [ "$1" = "--help" -o "$1" = "" ]; then
+ echo "ctl.sh { start | stop | --help }"
+ exit 0
+fi
+if [ "$1" = "start" ]; then
+ echo -n "Starting HBugs broker ... "
+ ./$daemon &> run/$daemon.log &
+ echo "done!"
+elif [ "$1" = "stop" ]; then
+ echo -n "Stopping HBugs broker ... "
+ killall -9 $daemon
+ echo "done!"
+fi
--- /dev/null
+#!/usr/bin/ocamlrun /usr/bin/ocaml
+(*
+ * Copyright (C) 2003-2004:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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/
+ *)
+#use "topfind"
+#require "pcre"
+#require "pxp"
+open Printf
+open Pxp_document
+open Pxp_dtd
+open Pxp_types
+open Pxp_yacc
+
+let index = "data/tutors_index.xml"
+let template = "data/hbugs_tutor.TPL.ml"
+
+ (* apply a set of regexp substitutions specified as a list of pairs
+ <pattern,template> to a string *)
+let rec apply_subst ~fill s =
+ match fill with
+ | [] -> s
+ | (pat, templ)::rest ->
+ apply_subst ~fill:rest (Pcre.replace ~pat ~templ s)
+ (* fill a ~template file with substitutions specified in ~fill (see
+ apply_subst) and save output to ~output *)
+let fill_template ~template ~fill ~output =
+ printf "Creating %s ... " output; flush stdout;
+ let (ic, oc) = (open_in template, open_out output) in
+ let rec fill_template' () =
+ output_string oc ((apply_subst ~fill (input_line ic)) ^ "\n");
+ fill_template' ()
+ in
+ try
+ output_string oc (sprintf
+"(*
+ THIS CODE IS GENERATED - DO NOT MODIFY!
+
+ the source of this code is template \"%s\"
+ the template was filled with data read from \"%s\"
+*)\n"
+ template index);
+ fill_template' ()
+ with End_of_file ->
+ close_in ic;
+ close_out oc;
+ printf "done!\n"; flush stdout
+let parse_xml fname =
+ parse_wfdocument_entity default_config (from_file fname) default_spec
+let is_tutor node =
+ match node#node_type with T_element "tutor" -> true | _ -> false
+let is_element node =
+ match node#node_type with T_element _ -> true | _ -> false
+let main () =
+ (parse_xml index)#root#iter_nodes
+ (fun node ->
+ try
+ (match node with
+ | node when is_tutor node ->
+ (try (* skip hand-written tutors *)
+ ignore (find_element "no_auto" node);
+ raise Exit
+ with Not_found -> ());
+ let output =
+ try
+ (match node#attribute "source" with
+ | Value s -> s
+ | _ -> assert false)
+ with Not_found -> assert false
+ in
+ let fill =
+ List.map (* create substitution list from index data *)
+ (fun node ->
+ let name = (* node name *)
+ (match node#node_type with
+ | T_element s -> s
+ | _ -> assert false)
+ in
+ let value = node#data in (* node value *)
+ (sprintf "@%s@" (String.uppercase name), (* pattern *)
+ value)) (* substitution *)
+ (List.filter is_element node#sub_nodes)
+ in
+ fill_template ~fill ~template ~output
+ | _ -> ())
+ with Exit -> ())
+
+let _ = main ()
+
--- /dev/null
+#!/usr/bin/ocamlrun /usr/bin/ocaml
+(*
+ * Copyright (C) 2003-2004:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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/
+ *)
+
+(* Usage: ls_tutors.ml # lists all tutors
+ * ls_tutors.ml -auto # lists only generated tutors
+ *)
+
+#use "topfind"
+#require "pxp"
+open Printf
+open Pxp_document
+open Pxp_dtd
+open Pxp_types
+open Pxp_yacc
+
+let index = "data/tutors_index.xml"
+let auto_only =
+ try
+ (match Sys.argv.(1) with "-auto" -> true | _ -> false)
+ with Invalid_argument _ -> false
+let parse_xml fname =
+ parse_wfdocument_entity default_config (from_file fname) default_spec
+let is_tutor node =
+ match node#node_type with T_element "tutor" -> true | _ -> false
+let main () =
+ List.iter
+ (fun tutor ->
+ try
+ (match tutor#attribute "source" with
+ | Value s ->
+ if not auto_only then
+ print_endline s
+ else (* we should print only generated tutors *)
+ (try
+ ignore (find_element "no_auto" tutor);
+ with Not_found ->
+ print_endline s)
+ | _ -> assert false)
+ with Not_found -> assert false)
+ (List.filter is_tutor (parse_xml index)#root#sub_nodes)
+let _ = main ()
+
--- /dev/null
+#!/bin/sh
+# Copyright (C) 2003:
+# Stefano Zacchiroli <zack@cs.unibo.it>
+# 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/
+if [ "$1" = "--help" -o "$1" = "" ]; then
+ echo "sabba.sh { start | stop | --help }"
+ exit 0
+fi
+
+./scripts/ls_tutors.ml |
+while read line; do
+ tutor=`echo $line | sed 's/\.ml//'`
+ if [ "$1" = "stop" ]; then
+ echo -n "Stopping HBugs tutor $tutor ... "
+ killall -9 $tutor
+ echo "done!"
+ elif [ "$1" = "start" ]; then
+ echo -n "Starting HBugs tutor $tutor ... "
+ nice -n 19 ./$tutor &> run/$tutor.log &
+ echo "done!"
+ else
+ echo "Uh? Try --help"
+ exit 1
+ fi
+done
--- /dev/null
+
+open Hbugs_types;;
+open Printf;;
+
+exception Empty_must;;
+
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
+
+let broker_id = ref None
+let my_own_id = Hbugs_tutors.init_tutor ()
+let my_own_addr, my_own_port = "127.0.0.1", 50011
+let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
+let environment_file = "search_pattern_apply.environment"
+let dump_environment_on_exit = false
+
+let is_authenticated id =
+ match !broker_id with
+ | None -> false
+ | Some broker_id -> id = broker_id
+
+ (* thread who do the dirty work *)
+let slave mqi_handle (state, musing_id) =
+ try
+ prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
+ let (proof, goal) = Hbugs_tutors.load_state state in
+ let hint =
+ try
+ let choose_must must only = (* euristic: use 2nd precision level
+ 1st is more precise but is more slow *)
+ match must with
+ | [] -> raise Empty_must
+ | _::hd::tl -> hd
+ | hd::tl -> hd
+ in
+ let uris =
+ TacticChaser.matchConclusion mqi_handle
+ ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
+ in
+ if uris = [] then
+ Sorry
+ else
+ Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
+ with Empty_must -> Sorry
+ in
+ let answer = Musing_completed (my_own_id, musing_id, hint) in
+ ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors.broker_url answer);
+ prerr_endline
+ (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
+ with
+ (Pxp_types.At _) as e ->
+ let rec unbox_exception =
+ function
+ Pxp_types.At (_,e) -> unbox_exception e
+ | e -> e
+ in
+ prerr_endline ("Uncaught PXP exception: " ^ Pxp_types.string_of_exn e) ;
+ (* e could be the Thread.exit exception; otherwise we will release an *)
+ (* uncaught exception and the Pxp_types.At was already an uncaught *)
+ (* exception ==> no additional arm *)
+ raise (unbox_exception e)
+
+let hbugs_callback mqi_handle =
+ let ids = Hashtbl.create 17 in
+ let forbidden () =
+ prerr_endline "ignoring request from unauthorized broker";
+ Exception ("forbidden", "")
+ in
+ function
+ | Start_musing (broker_id, state) ->
+ if is_authenticated broker_id then begin
+ prerr_endline "received Start_musing";
+ let new_musing_id = Hbugs_id_generator.new_musing_id () in
+ let id = ExtThread.create (slave mqi_handle) (state, new_musing_id) in
+ prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id);
+ Hashtbl.add ids new_musing_id id;
+ (*ignore (Thread.create slave (state, new_musing_id));*)
+ Musing_started (my_own_id, new_musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | Abort_musing (broker_id, musing_id) ->
+ prerr_endline "CSC: Abort_musing received" ;
+ if is_authenticated broker_id then begin
+ (* prerr_endline "Ignoring 'Abort_musing' message ..."; *)
+ (try
+ ExtThread.kill (Hashtbl.find ids musing_id) ;
+ Hashtbl.remove ids musing_id ;
+ with
+ Not_found
+ | ExtThread.Can_t_kill _ ->
+ prerr_endline ("Can not kill slave " ^ musing_id)) ;
+ Musing_aborted (my_own_id, musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | unexpected_msg ->
+ Exception ("unexpected_msg",
+ Hbugs_messages.string_of_msg unexpected_msg)
+
+let callback mqi_handle (req: Http_types.request) outchan =
+ try
+ let req_msg = Hbugs_messages.msg_of_string req#body in
+ let answer = hbugs_callback mqi_handle req_msg in
+ Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
+ with Hbugs_messages.Parse_error (subj, reason) ->
+ Http_daemon.respond
+ ~body:(Hbugs_messages.string_of_msg
+ (Exception ("parse_error", reason)))
+ outchan
+
+let restore_environment () =
+ let ic = open_in environment_file in
+ prerr_endline "Restoring environment ...";
+ CicEnvironment.restore_from_channel
+ ~callback:(fun uri -> prerr_endline uri) ic;
+ prerr_endline "... done!";
+ close_in ic
+
+let dump_environment () =
+ let oc = open_out environment_file in
+ prerr_endline "Dumping environment ...";
+ CicEnvironment.dump_to_channel
+ ~callback:(fun uri -> prerr_endline uri) oc;
+ prerr_endline "... done!";
+ close_out oc
+
+let main () =
+ try
+ Sys.catch_break true;
+ at_exit (fun () ->
+ if dump_environment_on_exit then
+ dump_environment ();
+ Hbugs_tutors.unregister_from_broker my_own_id);
+ broker_id :=
+ Some (Hbugs_tutors.register_to_broker
+ my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
+ let mqi_handle = MQIC.init ~log:prerr_string () in
+ if Sys.file_exists environment_file then
+ restore_environment ();
+ Http_daemon.start'
+ ~addr:my_own_addr ~port:my_own_port ~mode:`Thread (callback mqi_handle);
+ MQIC.close mqi_handle
+ with Sys.Break -> () (* exit nicely, invoking at_exit functions *)
+;;
+
+main ()
+
--- /dev/null
+*.cmi
+*.cmo
+*.cma
+*.cmx
+*.o
+*.a
+test_serialization
--- /dev/null
+<test>
+
+ <!-- general purpose -->
+
+ <help />
+
+ <usage>usage string</usage>
+
+ <exception name='eccezione1'>corpo dell'exc</exception>
+
+ <!-- client -> broker -->
+
+ <register_client id='client_id' url='client_url' />
+
+ <unregister_client id='client_id' />
+
+ <list_tutors id='client_id' />
+
+ <subscribe id='client_id'>
+ <tutor id='tutor_id1' />
+ <tutor id='tutor_id2' />
+ <!-- .... -->
+ <tutor id='tutor_idN' />
+ </subscribe>
+
+ <state_change id='client_id'> <!-- new state received -->
+ <gTopLevelStatus>
+ <CurrentGoal>0</CurrentGoal>
+ <ConstantType>
+ </ConstantType>
+ <CurrentProof>
+ </CurrentProof>
+ </gTopLevelStatus>
+ </state_change>
+
+ <state_change id='client_id'> <!-- no state received: proof is completed -->
+ <gTopLevelStatus />
+ </state_change>
+
+ <wow id="client_id" />
+
+ <!-- tutor -> broker -->
+
+ <register_tutor id='tutor_id' url='tutor_url'>
+ <hint_type>
+ <!-- HINT TYPE -->
+ </hint_type>
+ <description>
+ descrizione del tutor
+ </description>
+ </register_tutor>
+
+ <unregister_tutor id='tutor_id' />
+
+ <musing_started id='tutor_id' musing_id='musing_id' />
+
+ <musing_aborted id='tutor_id' musing_id='musing_id' />
+
+ <musing_completed id='tutor_id' musing_id='musing_id'>
+ <sorry />
+ </musing_completed>
+
+ <musing_completed id='tutor_id' musing_id='musing_id'>
+ <eureka>
+ <ring />
+ </eureka>
+ </musing_completed>
+
+ <musing_completed id='tutor_id' musing_id='musing_id'>
+ <eureka>
+ <hints>
+ <ring />
+ <fourier />
+ </hints>
+ </eureka>
+ </musing_completed>
+
+ <!-- broker -> client -->
+
+ <client_registered id='broker_id' />
+
+ <client_unregistered id='broker_id' />
+
+ <tutor_list id='broker_id'>
+ <tutor_dsc id='tutor_id1'> description 1 </tutor_dsc>
+ <tutor_dsc id='tutor_id2'> description 2 </tutor_dsc>
+ <!-- ... -->
+ <tutor_dsc id='tutor_idN'> description N </tutor_dsc>
+ </tutor_list>
+
+ <subscribed id='broker_id'>
+ <tutor_dsc id='tutor_id1'> description 1 </tutor_dsc>
+ <tutor_dsc id='tutor_id2'> description 2 </tutor_dsc>
+ <!-- ... -->
+ <tutor_dsc id='tutor_idN'> description N </tutor_dsc>
+ </subscribed>
+
+ <state_accepted id='broker_id'>
+ <stopped>
+ <musing id='musing_id1' />
+ <!-- ... -->
+ <musing id='musing_idN' />
+ </stopped>
+ <started>
+ <musing id='musing_id1' />
+ <!-- ... -->
+ <musing id='musing_idM' />
+ </started>
+ </state_accepted>
+
+ <hint id='broker_id'>
+ <ring />
+ </hint>
+
+ <hint id='broker_id'>
+ <hints>
+ <ring />
+ <fourier />
+ </hints>
+ </hint>
+
+ <!-- broker -> tutor -->
+
+ <tutor_registered id='broker_id' />
+
+ <tutor_unregistered id='broker_id' />
+
+ <start_musing id='broker_id'>
+ <gTopLevelStatus>
+ <CurrentGoal>0</CurrentGoal>
+ <ConstantType>
+ </ConstantType>
+ <CurrentProof>
+ </CurrentProof>
+ </gTopLevelStatus>
+ </start_musing>
+
+ <abort_musing id='broker_id' musing_id='musing_id' />
+
+ <thanks id='broker_id' musing_id='musing_id' />
+
+ <too_late id='broker_id' musing_id='musing_id' />
+
+</test>
--- /dev/null
+all: test_serialization
+test_serialization: test_serialization.ml
+ OCAMLPATH="../meta" ocamlfind ocamlc -linkpkg -package hbugs-common -o test_serialization test_serialization.ml
+clean:
+ rm -f *.cm[io] test_serialization
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 Pxp_document;;
+open Pxp_dtd;;
+open Pxp_types;;
+open Pxp_yacc;;
+
+open Printf;;
+
+let test_data = "HBUGS_MESSAGES.xml" ;;
+
+let test_message (n:('a Pxp_document.extension as 'b) Pxp_document.node as 'a) =
+ try
+ let msg_string =
+ let buf = Buffer.create 1000 in
+ n#write (`Out_buffer buf) `Enc_utf8;
+ Buffer.contents buf
+ in
+ let msg = Hbugs_messages.msg_of_string msg_string in
+ let pp = Hbugs_messages.string_of_msg msg in
+ let msg' = Hbugs_messages.msg_of_string pp in
+ if (msg <> msg') then
+ prerr_endline
+ (sprintf "Failure with msg %s"
+ (match n#node_type with T_element name -> name | _ -> assert false))
+ with e ->
+ prerr_endline
+ (sprintf "Failure with msg %s: uncaught exception %s"
+ (match n#node_type with T_element name -> name | _ -> assert false)
+ (Printexc.to_string e))
+;;
+
+let is_xml_element n =
+ match n#node_type with T_element _ -> true | _ -> false
+;;
+
+let root =
+ parse_wfcontent_entity default_config (from_file test_data) default_spec
+in
+printf "Testing all messages from %s ...\n" test_data; flush stdout;
+List.iter test_message (List.filter is_xml_element root#sub_nodes);
+printf "Done!\n"
+;;
+
projects / helm.git / commitdiff