+++ /dev/null
-DIRS = meta common broker client tutors
-
-DIRS_BYTE = $(patsubst %,%.byte,$(DIRS))
-DIRS_OPT = $(patsubst %,%.opt,$(DIRS))
-DIRS_CLEAN = $(patsubst %,%.clean,$(DIRS))
-DIRS_DISTCLEAN = $(patsubst %,%.distclean,$(DIRS))
-all: byte
-meta:
- $(MAKE) -C meta/
-byte: meta $(DIRS_BYTE)
-opt: meta $(DIRS_OPT)
-world: byte opt
-clean: $(DIRS_CLEAN)
-distclean: $(DIRS_DISTCLEAN)
-%.byte:
- $(MAKE) -C $*/ all
-%.opt:
- $(MAKE) -C $*/ opt
-%.clean:
- $(MAKE) -C $*/ clean
-%.distclean:
- $(MAKE) -C $*/ distclean
-start:
- $(MAKE) -C broker/ start
- $(MAKE) -C tutors/ start
-stop:
- $(MAKE) -C tutors/ stop
- $(MAKE) -C broker/ stop
-restart: stop start
-.PHONY: all byte opt world clean meta restart start stop
+++ /dev/null
-*.cmi
-*.cmo
-*.cma
-*.cmx
-*.o
-*.a
-hbugs_broker
-hbugs_broker.opt
+++ /dev/null
-hbugs_broker.cmo: hbugs_broker_registry.cmi
-hbugs_broker.cmx: hbugs_broker_registry.cmx
-hbugs_broker_registry.cmo: hbugs_broker_registry.cmi
-hbugs_broker_registry.cmx: hbugs_broker_registry.cmi
+++ /dev/null
-NAME = hbugs_broker
-METADIR = ../meta
-REQUIRES = http threads hbugs-common hbugs-thread-safe threads
-COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o
-OCAMLFIND = ocamlfind
-OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS)
-OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(COMMONOPTS)
-OCAMLDEP = $(OCAMLFIND) ocamldep $(COMMONOPTS)
-MODULES = hbugs_broker_registry
-OCAMLDOC = \
- ocamldoc \
- $(shell $(OCAMLFIND) query -i-format http) \
- $(shell $(OCAMLFIND) query -i-format threads) \
- $(shell $(OCAMLFIND) query -i-format hbugs-common) \
- $(shell $(OCAMLFIND) query -i-format hbugs-thread-safe) \
- $(shell $(OCAMLFIND) query -i-format hbugs-thread-safe) \
- $(shell $(OCAMLFIND) query -i-format pxp-engine) \
- $(shell $(OCAMLFIND) query -i-format pcre)
-CTL = ./hbugs_broker_ctl.sh
-
-OBJS = $(patsubst %,%.cmo,$(MODULES))
-OBJSOPT = $(patsubst %,%.cmx,$(MODULES))
-DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
-DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))
-
-all: byte
-byte: $(NAME)
-opt: $(NAME).opt
-world: byte opt
-start:
- $(CTL) start
-stop:
- $(CTL) stop
-
-include .depend
-depend:
- $(OCAMLDEP) *.ml *.mli > .depend
-
-%.cmi: %.mli
- $(OCAMLC) -c $<
-%.cmo: %.ml %.cmi
- $(OCAMLC) -c $<
-%.cmx: %.ml %.cmi
- $(OCAMLOPT) -c $<
-include Makefile.overrides
-$(OBJS): $(DEPS)
-$(OBJSOPT): $(DEPSOPT)
-$(NAME): $(OBJS) $(NAME).ml
- $(OCAMLC) -linkpkg -thread -o $@ $^
-$(NAME).opt: $(OBJSOPT) $(NAME).ml
- $(OCAMLOPT) -linkpkg -thread -o $@ $^
-$(NAME).dot: *.ml *.mli ../common/*.ml ../common/*.mli
- $(OCAMLDOC) -dot -o $@ $^
-
-distclean: clean
- rm -f run/*
-clean:
- rm -f *.cm[aiox] *.o $(NAME){,.opt}
-
-.PHONY: all byte opt world depend clean start 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
-#!/bin/sh
-daemon="hbugs_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
-(*
- * 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
-*.cmi
-*.cmo
-*.cma
-*.cmx
-*.o
-*.a
-hbugs_client_gui.ml
-hbugs_client
-hbugs_client.opt
+++ /dev/null
-NAME = hbugs_client
-METADIR = ../meta
-REQUIRES = lablgtk2 threads hbugs-common lablgtk2.glade
-PREDICATES = glade init
-COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
-OCAMLC = OCAMLPATH="$(METADIR)" ocamlfind ocamlc -thread $(COMMONOPTS)
-OCAMLOPT = OCAMLPATH="$(METADIR)" ocamlfind ocamlopt -thread $(COMMONOPTS)
-OCAMLFIND = ocamlfind
-
-DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
-DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))
-
-all: byte
-world: byte opt
-byte: $(NAME)
-opt: $(NAME).opt
-
-hbugs_client_gui.ml: hbugs_gui.glade
- lablgladecc2 $< > $@.tmp
- mv $@.tmp $@
-hbugs_client_gui.cmo: hbugs_client_gui.ml
- $(OCAMLC) -c $<
-hbugs_client_gui.cmx: hbugs_client_gui.ml
- $(OCAMLOPT) -c $<
-hbugs_client.cmi: hbugs_client.mli
- $(OCAMLC) -c $<
-hbugs_client.cmo: hbugs_client.ml hbugs_client.cmi
- $(OCAMLC) -thread -c $<
-hbugs_client.cmx: hbugs_client.ml hbugs_client.cmi
- $(OCAMLOPT) -thread -c $<
-$(NAME): $(DEPS) hbugs_client_gui.cmo $(NAME).cmo main.ml
- $(OCAMLC) -thread -package threads -linkpkg -o $@ hbugs_client_gui.cmo $(NAME).cmo main.ml
-$(NAME).opt: $(DEPSOPT) hbugs_client_gui.cmx $(NAME).cmx main.ml
- $(OCAMLOPT) -thread -package threads -linkpkg -o $@ hbugs_client_gui.cmx $(NAME).cmx main.ml
-clean:
- rm -f *.cm[aixo] *.cmxa *.[oa] $(NAME){,.opt} hbugs_client_gui.ml
-distclean: clean
-.PHONY: all world byte opt clean
+++ /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_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
-*.cmi
-*.cmo
-*.cma
-*.cmx
-*.o
-*.a
+++ /dev/null
-hbugs_common.cmo: hbugs_types.cmo hbugs_common.cmi
-hbugs_common.cmx: hbugs_types.cmx 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.cmo hbugs_messages.cmi
-hbugs_messages.cmx: hbugs_misc.cmx hbugs_types.cmx hbugs_messages.cmi
-hbugs_misc.cmo: hbugs_misc.cmi
-hbugs_misc.cmx: hbugs_misc.cmi
-hbugs_common.cmi: hbugs_types.cmo
-hbugs_id_generator.cmi: hbugs_types.cmo
-hbugs_messages.cmi: hbugs_types.cmo
+++ /dev/null
-REQUIRES = helm-xml helm-pxp pcre pxp http
-COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o
-OCAMLFIND = ocamlfind
-OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS)
-OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(COMMONOPTS)
-OCAMLDEP = $(OCAMLFIND) ocamldep $(COMMONOPTS)
-OCAMLDOC = \
- ocamldoc \
- $(shell $(OCAMLFIND) query -i-format helm-xml) \
- $(shell $(OCAMLFIND) query -i-format helm-pxp) \
- $(shell $(OCAMLFIND) query -i-format pcre) \
- $(shell $(OCAMLFIND) query -i-format pxp-engine) \
- $(shell $(OCAMLFIND) query -i-format threads) \
- $(shell $(OCAMLFIND) query -i-format http)
-MODULES = \
- hbugs_types threadSafe hbugs_misc \
- hbugs_common hbugs_id_generator hbugs_messages
-
-OBJS = $(patsubst %,%.cmo,$(MODULES))
-OBJSOPT = $(patsubst %,%.cmx,$(MODULES))
-DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
-DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))
-
-all: byte
-byte: $(OBJS)
-opt: $(OBJSOPT)
-world: byte opt
-
-hbugs_common.dot: *.ml *.mli
- $(OCAMLDOC) -dot -o $@ $^
-
-include .depend
-depend:
- $(OCAMLDEP) *.ml *.mli > .depend
-
-%.cmi: %.mli
- $(OCAMLC) -c $<
-%.cmo: %.ml %.cmi
- $(OCAMLC) -c $<
-%.cmx: %.ml %.cmi
- $(OCAMLOPT) -c $<
-include Makefile.overrides
-$(OBJS): $(DEPS)
-$(OBJSOPT): $(DEPSOPT)
-
-distclean: clean
-clean:
- rm -f *.cm[aiox] *.o $(NAME){,.opt}
-
-.PHONY: all byte opt world depend clean
-
+++ /dev/null
-hbugs_types.cmi hbugs_types.cmo: hbugs_types.ml
- $(OCAMLC) -c $<
-threadSafe.cmi threadSafe.cmo: threadSafe.ml
- $(OCAMLC) -thread -package threads -c $<
-threadSafe.cmx: threadSafe.ml threadSafe.cmi
- $(OCAMLOPT) -thread -package threads -c $<
+++ /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 msg_of_string' s =
- let root = (* xml tree's root *)
- parse_wfcontent_entity default_config (from_string s) default_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/
- *)
-
-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
-(*
- * 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 debug_print = let debug = false in fun s -> if debug then prerr_endline s;;
-
-class threadSafe =
- object (self)
-
- val mutex = Mutex.create ()
-
- (** condition variable: 'no readers is currently reading' *)
- val noReaders = Condition.create ()
-
- (** readers count *)
- val mutable readersCount = 0
-
- method private incrReadersCount = (* internal, not exported *)
- self#doCritical (lazy (
- readersCount <- readersCount + 1
- ))
-
- method private decrReadersCount = (* internal, not exported *)
- self#doCritical (lazy (
- if readersCount > 0 then readersCount <- readersCount - 1;
- ))
-
- method private signalNoReaders = (* internal, not exported *)
- self#doCritical (lazy (
- if readersCount = 0 then Condition.signal noReaders
- ))
-
- method private doCritical: 'a. 'a lazy_t -> 'a =
- fun action ->
- debug_print "<doCritical>";
- (try
- Mutex.lock mutex;
- let res = Lazy.force action in
- Mutex.unlock mutex;
- debug_print "</doCritical>";
- res
- with e ->
- Mutex.unlock mutex;
- raise e);
-
- method private doReader: 'a. 'a lazy_t -> 'a =
- fun action ->
- debug_print "<doReader>";
- let cleanup () =
- self#decrReadersCount;
- self#signalNoReaders
- in
- self#incrReadersCount;
- let res = (try Lazy.force action with e -> (cleanup (); raise e)) in
- cleanup ();
- debug_print "</doReader>";
- res
-
- (* TODO may starve!!!! is what we want or not? *)
- method private doWriter: 'a. 'a lazy_t -> 'a =
- fun action ->
- debug_print "<doWriter>";
- self#doCritical (lazy (
- while readersCount > 0 do
- Condition.wait noReaders mutex
- done;
- let res = Lazy.force action in
- debug_print "</doWriter>";
- res
- ))
-
- end
+++ /dev/null
-META.hbugs-common
-META.hbugs-client
-META.hbugs-thread-safe
+++ /dev/null
-requires="pcre pxp http hbugs-common lablgtk2.glade"
-directory="@HBUGS_CLIENT_DIR@"
-archive(byte) = "hbugs_client_gui.cmo hbugs_client.cmo"
-archive(native) = "hbugs_client_gui.cmx hbugs_client.cmx"
+++ /dev/null
-requires="pcre pxp http"
-directory="@HBUGS_COMMON_DIR@"
-archive(byte) = "hbugs_types.cmo hbugs_misc.cmo hbugs_common.cmo hbugs_id_generator.cmo hbugs_messages.cmo"
-archive(native) = "hbugs_types.cmx hbugs_misc.cmx hbugs_common.cmx hbugs_id_generator.cmx hbugs_messages.cmx"
+++ /dev/null
-requires="threads"
-directory="@HBUGS_COMMON_DIR@"
-archive(byte) = "threadSafe.cmo"
-archive(native) = "threadSafe.cmx"
+++ /dev/null
-META = META.hbugs-common META.hbugs-thread-safe META.hbugs-client
-all: $(META)
-opt:
-META.hbugs-common: META.hbugs-common.in
- sed 's%@HBUGS_COMMON_DIR@%$(CURDIR)/../common%' < $< > $@
-META.hbugs-thread-safe: META.hbugs-thread-safe.in
- sed 's%@HBUGS_COMMON_DIR@%$(CURDIR)/../common%' < $< > $@
-META.hbugs-client: META.hbugs-client.in
- sed 's%@HBUGS_CLIENT_DIR@%$(CURDIR)/../client%' < $< > $@
-clean:
-distclean: clean
- rm -f $(META)
+++ /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"
-;;
-
+++ /dev/null
-*.environment
-*.cmi
-*.cmo
-*.cma
-*.cmx
-*.o
-*.a
-*.opt
-ring_tutor.ml
-fourier_tutor.ml
-reflexivity_tutor.ml
-symmetry_tutor.ml
-assumption_tutor.ml
-contradiction_tutor.ml
-exists_tutor.ml
-split_tutor.ml
-left_tutor.ml
-right_tutor.ml
-ring_tutor
-fourier_tutor
-reflexivity_tutor
-symmetry_tutor
-assumption_tutor
-contradiction_tutor
-exists_tutor
-split_tutor
-left_tutor
-right_tutor
-search_pattern_apply_tutor
+++ /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
-METADIR = ../meta
-REQUIRES = threads hbugs-common helm-cic_proof_checking helm-getter \
- helm-cic_textual_parser \
- helm-mathql helm-mathql_interpreter helm-tactics
-COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
-OCAMLFIND = ocamlfind
-OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS)
-OCAMLOPT = $(OCAMLFIND) opt -thread $(COMMONOPTS)
-OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)"
-LINK_OPTIONS = -thread -package threads -linkpkg
-TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
-TUTORS_INDEX = INDEX.xml
-GENERATED_TUTORS = \
- ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \
- assumption_tutor contradiction_tutor exists_tutor split_tutor \
- left_tutor right_tutor
-TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor
-BUILD_TUTORS = ./build_tutors.ml
-CTL = ./sabba.sh
-TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
-GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
-COMMON = hbugs_deity.cmo hbugs_tutors_common.cmo
-COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON))
-
-DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
-DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))
-
-all: byte
-world: byte opt
-byte: $(COMMON) $(TUTORS)
-opt: $(COMMON_OPT) $(TUTORS_OPT)
-start:
- $(CTL) start
-stop:
- $(CTL) stop
-
-$(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
- $(BUILD_TUTORS)
-%_tutor: $(DEPS) $(COMMON) %_tutor.ml
- $(OCAMLC) $(LINK_OPTIONS) -o $@ $(COMMON) $*_tutor.ml
-%_tutor.opt: $(DEPSOPT) $(COMMON_OPT) %_tutor.ml
- $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $(COMMON_OPT) $*_tutor.ml
-
-%.cmi: %.mli
- $(OCAMLC) -c $<
-%.cmo: %.ml %.cmi
- $(OCAMLC) -c $<
-%.cmx: %.ml %.cmi
- $(OCAMLOPT) -c $<
-
-clean:
- rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
-distclean: clean
- rm -f run/*
-.PHONY: all world byte opt clean start stop
-.PRECIOUS: %.cmi
-
+++ /dev/null
-#!/usr/bin/ocamlrun /usr/bin/ocaml
-(*
- * 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/
- *)
-#use "topfind";;
-#require "pcre";;
-#require "pxp";;
-open Printf;;
-open Pxp_document;;
-open Pxp_dtd;;
-open Pxp_types;;
-open Pxp_yacc;;
-
-let index = "INDEX.xml" ;;
-let template = "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
-;;
-exception Skip;;
-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 Skip
- 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 Skip -> ())
-;;
-main ();;
-
+++ /dev/null
-(*
- * 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/
- *)
-
-let debug = true
-let debug_print s = if debug then prerr_endline s
-
-exception Can_t_kill of Thread.t * string (* thread, reason *)
-exception Thread_not_found of Thread.t
-
-module OrderedPid =
- struct
- type t = int
- let compare = Pervasives.compare
- end
-module PidSet = Set.Make (OrderedPid)
-
- (* perform an action inside a critical section controlled by given mutex *)
-let do_critical mutex =
- fun action ->
- try
- Mutex.lock mutex;
- let res = Lazy.force action in
- Mutex.unlock mutex;
- res
- with e -> Mutex.unlock mutex; raise e
-
-let kill_signal = Sys.sigusr2 (* signal used to kill children *)
-let chan = Event.new_channel () (* communication channel between threads *)
-let creation_mutex = Mutex.create ()
-let dead_threads_walking = ref PidSet.empty
-let pids: (Thread.t, int) Hashtbl.t = Hashtbl.create 17
-
- (* given a thread body (i.e. first argument of a Thread.create invocation)
- return a new thread body which unblock the kill signal and send its pid to
- parent over "chan" *)
-let wrap_thread body =
- fun arg ->
- ignore (Unix.sigprocmask Unix.SIG_UNBLOCK [ kill_signal ]);
- Event.sync (Event.send chan (Unix.getpid ()));
- body arg
-
-(*
-(* FAKE IMPLEMENTATION *)
-let create = Thread.create
-let kill _ = ()
-*)
-
-let create body arg =
- do_critical creation_mutex (lazy (
- let thread_t = Thread.create (wrap_thread body) arg in
- let pid = Event.sync (Event.receive chan) in
- Hashtbl.add pids thread_t pid;
- thread_t
- ))
-
-let kill thread_t =
- try
- let pid =
- try
- Hashtbl.find pids thread_t
- with Not_found -> raise (Thread_not_found thread_t)
- in
- dead_threads_walking := PidSet.add pid !dead_threads_walking;
- Unix.kill pid kill_signal
- with e -> raise (Can_t_kill (thread_t, Printexc.to_string e))
-
- (* "kill_signal" handler, check if current process must die, if this is the
- case exits with Thread.exit *)
-let _ =
- ignore (Sys.signal kill_signal (Sys.Signal_handle
- (fun signal ->
- let myself = Unix.getpid () in
- match signal with
- | sg when (sg = kill_signal) &&
- (PidSet.mem myself !dead_threads_walking) ->
- dead_threads_walking := PidSet.remove myself !dead_threads_walking;
- debug_print "AYEEEEH!";
- Thread.exit ()
- | _ -> ())))
-
- (* block kill signal in main process *)
-let _ = ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ])
-
+++ /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/
- *)
-
-exception Can_t_kill of Thread.t * string
-
-val create: ('a -> 'b) -> 'a -> Thread.t
-val kill: Thread.t -> 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/
- *)
-
-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_common.BuildTutor (TutorDescription) ;;
-Tutor.start () ;;
-
+++ /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 =
- Hbugs_deity.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
- Hbugs_deity.kill slave_thread;
- Hashtbl.remove slaves musing_id
- with
- | Hbugs_deity.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
-#!/usr/bin/ocamlrun /usr/bin/ocaml
-(*
- * 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/
- *)
-#use "topfind";;
-#require "pxp";;
-open Printf;;
-open Pxp_document;;
-open Pxp_dtd;;
-open Pxp_types;;
-open Pxp_yacc;;
-
-let index = "INDEX.xml" ;;
-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 -> print_endline s
- | _ -> assert false)
- with Not_found -> assert false)
- (List.filter is_tutor (parse_xml index)#root#sub_nodes)
-;;
-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
-
-./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_common.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_common.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_common.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 = Hbugs_deity.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
- Hbugs_deity.kill (Hashtbl.find ids musing_id) ;
- Hashtbl.remove ids musing_id ;
- with
- Not_found
- | Hbugs_deity.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_common.unregister_from_broker my_own_id);
- broker_id :=
- Some (Hbugs_tutors_common.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 ()
-
projects / helm.git / commitdiff