containing an optional string, used to identify associated user.
(* CSC: new NCicPp.status is the best I can do here
without changing the return type *)
Ast.fail loc (sprintf "Argument %s not found"
- (NotationPp.pp_term (new NCicPp.status) name))
+ (NotationPp.pp_term (new NCicPp.status None) name))
| (l,_) :: tl ->
(match position_of name 0 l with
| None, len -> find_arg name (n + len) tl
db.loctable := CicNotationLexer.LocalizeEnv.empty
end
-class virtual status ~keywords:kwds =
+class virtual status uid ~keywords:kwds =
object
- inherit NCic.status
+ inherit NCic.status uid
inherit status0 kwds
end
method notation_parser_db: db
end
-class virtual status: keywords:string list ->
+class virtual status: string option -> keywords:string list ->
object('self)
inherit NCic.status
inherit g_status
(* Debugging only *)
(*CSC: new NCicPp.status is the best I can do now *)
- let string_of_term = NotationPp.pp_term (new NCicPp.status)
- let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
+ (*WR: can't guess a user id so I must use None *)
+ let string_of_term = NotationPp.pp_term (new NCicPp.status None)
+ let string_of_pattern = NotationPp.pp_term (new NCicPp.status None)
end
module M = PatternMatcher.Matcher (Pattern21)
method content_pres_db: db
end
-class virtual status =
+class virtual status uid =
object
- inherit NCic.status
+ inherit NCic.status uid
val content_pres_db = initial_db
method content_pres_db = content_pres_db
method set_content_pres_db v = {< content_pres_db = v >}
end
class virtual status :
+ string option ->
object ('self)
inherit NCic.status
method content_pres_db: db
let command_error msg = raise (Command_error msg)
-class virtual status = fun (b : string) ->
+class virtual status = fun (uid : string option) (b : string) ->
let fake_obj =
NUri.uri_of_string "cic:/matita/dummy.decl",0,[],[],
NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular))
in
object
(* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
- inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
+ inherit ([Continuationals.Stack.t] NTacStatus.status uid fake_obj (Continuationals.Stack.empty))
inherit NCicLibrary.dumpable_status
- inherit NCicLibrary.status
- inherit GrafiteDisambiguate.status
- inherit GrafiteParser.status
- inherit TermContentPres.status
+ inherit NCicLibrary.status uid
+ inherit GrafiteDisambiguate.status uid
+ inherit GrafiteParser.status uid
+ inherit TermContentPres.status uid
val baseuri = b
val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
method baseuri = baseuri
type dumpable_s = status
let get status = (status : #status :> NCicLibrary.dumpable_status)
let set (status : dumpable_s) dump_status = status#set_dumpable_status dump_status
+ let user (status : dumpable_s) = status#user
end)
val command_error: string -> 'a (** @raise Command_error *)
class virtual status :
- string ->
+ string option -> string ->
object ('self)
(* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
inherit NTacStatus.tac_status
| _ ->
(*CSC: new NCicPp.status is the best I can do here without changing the
result type *)
- raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term (new NCicPp.status) params)) ]
+ raise (Invalid_argument ("malformed target parameter list 2\n" ^
+ NotationPp.pp_term (new NCicPp.status None ) params)) ]
];
direction: [
[ SYMBOL ">" -> `LeftToRight
method parser_db: db
end
-class virtual status =
+class virtual status uid =
object(self)
- inherit CicNotationParser.status ~keywords:[]
+ inherit CicNotationParser.status uid ~keywords:[]
val mutable db = None (* mutable only to initialize it :-( *)
method parser_db = match db with None -> assert false | Some x -> x
method set_parser_db v = {< db = Some v >}
end
class virtual status :
+ string option ->
object('self)
inherit g_status
inherit CicNotationParser.status
method interp_db: db
end
-class virtual status =
+class virtual status uid =
object(self)
- inherit NCicCoercion.status
+ inherit NCicCoercion.status uid
val mutable interp_db = None (* mutable only to initialize it :-( *)
method interp_db = match interp_db with None -> assert false | Some x -> x
method set_interp_db v = {< interp_db = Some v >}
end
class virtual status :
+ string option ->
object ('self)
inherit g_status
inherit NCicCoercion.status
(* Debugging functions only *)
let string_of_pattern = NotationPp.pp_cic_appl_pattern
+
+ (* WR: hope it's safe to pass userid=None to NCicPp.status *)
let string_of_term t =
- (new NCicPp.status)#ppterm ~metasenv:[] ~subst:[] ~context:[] t
+ (new NCicPp.status None)#ppterm ~metasenv:[] ~subst:[] ~context:[] t
let classify = function
| Ast.ImplicitPattern
method disambiguate_db: db
end
-class virtual status =
+class virtual status uid =
object (self)
- inherit Interpretations.status
+ inherit Interpretations.status uid
val disambiguate_db = initial_status
method disambiguate_db = disambiguate_db
method set_disambiguate_db v = {< disambiguate_db = v >}
end
class virtual status :
+ string option ->
object ('self)
inherit g_status
inherit Interpretations.status
type obj = NUri.uri * int * metasenv * substitution * obj_kind
(* pretty-printing *)
-class virtual status =
+class virtual status (uid : string option) =
object
+ method user = uid
+
method virtual ppterm: context:context -> subst:substitution ->
metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
let history = ref [];;
let frozen_list = ref [];;
-let get_obj = ref (fun _ _ -> assert false);;
+let get_obj = ref (fun _ _ -> assert false) ;;
let set_get_obj = (:=) get_obj;;
module F = Format
let ppobj status obj = on_buffer (ppobj status) obj;;
-class status =
+class status (uid : string option) =
object(self)
(* this method is meant to be overridden in ApplyTransformation *)
+ method user = uid
method ppterm = ppterm self
method ppcontext = ppcontext self
method ppmetasenv = ppmetasenv self
(* low-level pretty printer;
all methods are meant to be overridden in ApplyTransformation *)
-class status: NCic.cstatus
+class status: string option -> NCic.cstatus
(* variants that use a formatter
module Format : sig
NCicUntrusted.map_obj_kind (refresh_uri_in_term status) obj_kind
;;
-let ng_path_of_baseuri ?(no_suffix=false) baseuri =
+let ng_path_of_baseuri ?(no_suffix=false) user baseuri =
let uri = NUri.string_of_uri baseuri in
let path = String.sub uri 4 (String.length uri - 4) in
+ let path = match user with
+ | Some u -> "/" ^ u ^ path
+ | _ -> path
+ in
let path = Helm_registry.get "matita.basedir" ^ path in
let dirname = Filename.dirname path in
HExtlib.mkdir dirname;
dump
;;
-let require0 ~baseuri = require_path (ng_path_of_baseuri baseuri)
+let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri)
let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
let init = load_db;;
-class virtual status =
+class virtual status uid =
object
- inherit NCic.status
+ inherit NCic.status uid
val timestamp = (time0 : timestamp)
method timestamp = timestamp
method set_timestamp v = {< timestamp = v >}
method dump: dump
end
+(* uid = None --> single user mode *)
class dumpable_status =
object
val db = { objs = []; includes = []; dependencies = [] }
val require:
baseuri:NUri.uri -> fname:string -> alias_only:bool ->
dumpable_status -> dumpable_status
- val dependencies_of: baseuri:NUri.uri -> string list
+ val dependencies_of: string option -> baseuri:NUri.uri -> string list
end
-module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status val set: dumpable_s -> dumpable_status -> dumpable_s end) =
+module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
+ val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
+ string option end) =
struct
type dumpable_status = D.dumpable_s
type 'a register_type =
end
let serialize ~baseuri status =
- let status = D.get status in
- let ch = open_out (ng_path_of_baseuri baseuri) in
- Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) [];
+ let ch = open_out (ng_path_of_baseuri (D.user status) baseuri) in
+ Marshal.to_channel ch (magic,((D.get status)#dump.dependencies,(D.get status)#dump.objs)) [];
close_out ch;
List.iter
(function
| `Obj (uri,obj) ->
- let ch = open_out (ng_path_of_baseuri uri) in
+ let ch = open_out (ng_path_of_baseuri (D.user status) uri) in
Marshal.to_channel ch (magic,obj) [];
close_out ch
| `Constr _ -> ()
) !storage;
set_global_aliases (!local_aliases @ get_global_aliases ());
- List.iter (fun u -> add_deps u [baseuri]) status#dump.includes;
+ List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes;
time_travel0 time0
let require2 ~baseuri ~alias_only status =
(s#set_dump
{s#dump with
includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in
- let _dependencies,dump = require0 ~baseuri in
+ let _dependencies,dump = require0 (D.user status) ~baseuri in
List.fold_right (!require1 ~alias_only) dump status
with
Sys_error _ ->
- raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+ raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.user status) baseuri,NUri.string_of_uri baseuri))
- let dependencies_of ~baseuri = fst (require0 ~baseuri)
+ let dependencies_of user ~baseuri = fst (require0 user ~baseuri)
let record_include =
let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
objs = record_include (baseuri,fname)::s#dump.objs })
end
-let fetch_obj status uri =
- let obj = require0 ~baseuri:uri in
+let fetch_obj user status uri =
+ let obj = require0 user ~baseuri:uri in
refresh_uri_in_obj status obj
;;
(function `Obj (u,o) -> Some (u,o) | _ -> None )
!storage)
with Not_found ->
- try fetch_obj status u
+ try fetch_obj (status#user) status u
with Sys_error _ ->
raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
;;
type timestamp
class virtual status :
+ string option ->
object ('self)
inherit NCic.status
method timestamp: timestamp
method dump: dump
end
-class dumpable_status :
+class dumpable_status :
object ('self)
inherit g_dumpable_status
method set_dump: dump -> 'self
val require: baseuri:
NUri.uri -> fname:string -> alias_only:bool ->
dumpable_status -> dumpable_status
- val dependencies_of: baseuri:NUri.uri -> string list
+ val dependencies_of: string option -> baseuri:NUri.uri -> string list
end
-module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status val set: dumpable_s -> dumpable_status -> dumpable_s end) :
- SerializerType with type dumpable_status = D.dumpable_s
+module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
+ val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
+ string option end) :
+ SerializerType with type dumpable_status = D.dumpable_s
val refresh_uri: NUri.uri -> NUri.uri
-val ng_path_of_baseuri: ?no_suffix:bool -> NUri.uri -> string
+val ng_path_of_baseuri: ?no_suffix:bool -> string option -> NUri.uri -> string
(* EOF *)
let compare x y =
(* CSC: NCicPp.status is the best I can put here *)
- if NCicReduction.alpha_eq (new NCicPp.status) [] [] [] x y then 0
+ (* WR: and I can't guess a user id, so I must put None *)
+ if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y then 0
(* if x = y then 0 *)
else compare x y
;;
let pp t =
(* CSC: NCicPp.status is the best I can put here *)
- (new NCicPp.status)#ppterm ~context:C.context
+ (* WR: and I can't guess a user id, so I must put None *)
+ (new NCicPp.status None)#ppterm ~context:C.context
~metasenv:C.metasenv ~subst:C.subst t;;
type input = NCic.term
let saturate t ty =
let sty, _, args =
(* CSC: NCicPp.status is the best I can put here *)
- NCicMetaSubst.saturate (new NCicPp.status) ~delta:0 C.metasenv C.subst
+ (* WR: and I can't guess a user id, so I must put None *)
+ NCicMetaSubst.saturate (new NCicPp.status None) ~delta:0 C.metasenv C.subst
C.context ty 0
in
let proof =
method coerc_db: db
end
-class virtual status =
+class virtual status uid =
object
- inherit NCicUnifHint.status
+ inherit NCicUnifHint.status uid
val db = empty_db
method coerc_db = db
method set_coerc_db v = {< db = v >}
end
class virtual status :
+ string option ->
object ('self)
inherit g_status
inherit NCicUnifHint.status
method uhint_db: db
end
-class virtual status =
+class virtual status (uid : string option) =
object
- inherit NCic.status
+ inherit NCic.status uid
val db = HDB.empty, EQDB.empty
method uhint_db = db
method set_uhint_db v = {< db = v >}
end
class virtual status :
+ string option ->
object ('self)
inherit g_status
inherit NCic.status
method obj: NCic.obj
end
-class virtual pstatus =
+class virtual pstatus uid =
fun (o: NCic.obj) ->
object (self)
- inherit GrafiteDisambiguate.status
+ inherit GrafiteDisambiguate.status uid
inherit auto_status
inherit eq_status
val obj = o
method stack: 'stack
end
-class virtual ['stack] status =
+class virtual ['stack] status uid =
fun (o: NCic.obj) (s: 'stack) ->
object (self)
- inherit (pstatus o)
+ inherit (pstatus uid o)
val stack = s
method stack = stack
method set_stack s = {< stack = s >}
end
class virtual pstatus :
- NCic.obj ->
+ string option -> NCic.obj ->
object ('self)
inherit g_pstatus
inherit GrafiteDisambiguate.status
end
class virtual ['stack] status :
- NCic.obj -> 'stack ->
+ string option -> NCic.obj -> 'stack ->
object ('self)
inherit ['stack] g_status
inherit pstatus
(* CSC: potential bug here: the new methods still use the instance variables
of the old status and not the instance variables of the new one *)
let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStatus.status =
+ let uid = status#user in
let o =
object
- inherit ['b] NTacStatus.status status#obj stack
+ inherit ['b] NTacStatus.status uid status#obj stack
method ppterm = status#ppterm
method ppcontext = status#ppcontext
method ppsubst = status#ppsubst
lablgtk2.glade \
lablgtksourceview2.gtksourceview2 \
"
-# FIXME: we currently depend from some GTK libraries
-# this should be fixed!!!
FINDLIB_WREQUIRES="\
$FINDLIB_CREQUIRES \
netcgi2 \
nethttpd \
+uuidm \
"
-for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
+for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES $FINDLIB_WREQUIRES
do
AC_MSG_CHECKING(for $r ocaml library)
if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
lablGraphviz.cmo: lablGraphviz.cmi
lablGraphviz.cmx: lablGraphviz.cmi
+matitaAuthentication.cmo: matitaEngine.cmi matitaAuthentication.cmi
+matitaAuthentication.cmx: matitaEngine.cmx matitaAuthentication.cmi
matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi
matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx
-matitadaemon.cmo: matitaGtkMisc.cmi matitaEngine.cmi applyTransformation.cmi
-matitadaemon.cmx: matitaGtkMisc.cmx matitaEngine.cmx applyTransformation.cmx
+matitadaemon.cmo: matitaInit.cmi matitaEngine.cmi matitaAuthentication.cmi \
+ applyTransformation.cmi
+matitadaemon.cmx: matitaInit.cmx matitaEngine.cmx matitaAuthentication.cmx \
+ applyTransformation.cmx
matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
applyTransformation.cmi:
cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
lablGraphviz.cmi:
+matitaAuthentication.cmi: matitaEngine.cmi
matitaclean.cmi:
matitaEngine.cmi: applyTransformation.cmi
matitaExcPp.cmi:
include ../Makefile.defs
NULL =
-#H=@
+H=@
ifeq ($(ANNOT),true)
ANNOTOPTION = -dtypes
ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml)
# objects for matitac (batch compiler)
CML = buildTimeConf.ml $(CMLI:%.mli=%.ml)
+WML = matitaAuthentication.ml $(CML)
MAINCML = $(MAINCMLI:%.mli=%.ml)
PROGRAMS_BYTE = \
matitaScriptLexer.cmo: SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
+matitaAuthentication.cmi: matitaAuthentication.mli
+ $(H)echo " OCAMLC $<"
+ $(H)$(OCAMLC) $(WPKGS) -c $<
+matitaAuthentication.cmo: matitaAuthentication.ml
+ $(H)echo " OCAMLC $<"
+ $(H)$(OCAMLC) $(WPKGS) -c $<
+
CMOS = $(ML:%.ml=%.cmo)
CCMOS = $(CML:%.ml=%.cmo)
+WCMOS = $(WML:%.ml=%.cmo)
MAINCMOS = $(MAINCML:%.ml=%.cmo)
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
+WCMXS = $(patsubst %.cmo,%.cmx,$(WCMOS))
MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
$(CMOS) : $(LIB_DEPS)
$(CMXOS): $(LIBX_DEPS)
$(H)echo " OCAMLC matitac.ml"
$(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml
$(H)echo " OCAMLC matitadaemon.ml"
- $(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml
+ $(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(WCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml
.PHONY: linkonly
matita: matita.ml $(LIB_DEPS) $(CMOS)
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
-matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(CCMOS) $(MAINCMOS)
+matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(WCMOS) $(MAINCMOS)
$(H)echo " OCAMLC $<"
- $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitadaemon.ml
-matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(CCMXS) $(MAINCMXS)
+ $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(WCMOS) $(MAINCMOS) matitadaemon.ml
+matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(WCMXS) $(MAINCMXS)
$(H)echo " OCAMLOPT $<"
- $(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitadaemon.ml
+ $(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(WCMXS) $(MAINCMXS) matitadaemon.ml
rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
$(H)echo " OCAMLC $<"
*)
-class status =
+class status uid =
object(self)
- inherit Interpretations.status
- inherit TermContentPres.status
- inherit NCicPp.status
+ inherit Interpretations.status uid
+ inherit TermContentPres.status uid
+ inherit NCicPp.status uid
(*
method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
NCicPp.ppterm ~metasenv ~subst ~context t
val use_high_level_pretty_printer: bool ref
class status :
+ string option ->
object
inherit NCic.cstatus
inherit Interpretations.status
--- /dev/null
+(* Copyright (C) 2004-2011, HELM Team.
+ *
+ * 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 session_id = Uuidm.t
+
+(* user table: user id, (password, optional session id) *)
+type user = string * (string * session_id option)
+
+let user_tbl = (ref [] : user list ref)
+
+(* session table: (user id, session id), matita status *)
+type session = (string * session_id) * MatitaEngine.status
+
+let session_tbl = (ref [] : session list ref)
+
+exception UsernameCollision of string
+
+let lookup_user uid = List.assoc uid !user_tbl
+
+let create_session uid status =
+ let pw,sid = List.assoc uid !user_tbl in
+ let clean_utbl = List.remove_assoc uid !user_tbl in
+ let new_session = Uuidm.create `V4 in
+ user_tbl := (uid,(pw,Some new_session))::clean_utbl;
+ let clean_stbl = match sid with
+ | Some sid' ->
+ List.remove_assoc (uid,sid') !session_tbl
+ | _ -> !session_tbl
+ in session_tbl := ((uid,new_session),status)::clean_stbl
+;;
+
+let logout_user uid =
+ match List.assoc uid !user_tbl with
+ | _,None -> ()
+ | pw, Some sid ->
+ user_tbl := (uid,(pw,None))::List.remove_assoc uid !user_tbl;
+ session_tbl := List.remove_assoc (uid,sid) !session_tbl
+;;
+
+let remove_user uid =
+ user_tbl := List.remove_assoc uid !user_tbl
+;;
+
+(* serialization and deserialization of the user table *)
+let config_path () =
+ let path = Helm_registry.get "matita.basedir" in
+ let dirname = Filename.dirname path in
+ HExtlib.mkdir dirname;
+ path
+;;
+
+let serialize () =
+ let clean_utbl = List.map (fun (uid,(pw,_)) -> uid,(pw,None)) !user_tbl in
+ let utbl_ch = open_out (config_path () ^ "/usertable.dump") in
+ Marshal.to_channel utbl_ch clean_utbl [];
+ close_out utbl_ch;
+;;
+
+let deserialize () =
+ let utbl_ch = open_in (config_path () ^ "/usertable.dump") in
+ user_tbl := Marshal.from_channel utbl_ch;
+ close_in utbl_ch;
+ (* old_sessions are now invalid *)
+ session_tbl := [];
+;;
+
+let add_user uid pw =
+ try
+ let _ = lookup_user uid in
+ raise (UsernameCollision uid)
+ with Not_found ->
+ user_tbl := (uid,(pw,None))::!user_tbl;
+ serialize ()
+;;
--- /dev/null
+(* Copyright (C) 2004-2011, HELM Team.
+ *
+ * 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 session_id = Uuidm.t
+
+exception UsernameCollision of string
+
+val lookup_user : string -> (string * session_id option)
+
+val create_session : string -> MatitaEngine.status -> unit
+
+val logout_user : string -> unit
+
+val remove_user : string -> unit
+
+val serialize : unit -> unit
+
+val deserialize : unit -> unit
+
+val add_user : string -> string -> unit
open GrafiteTypes
open Printf
-class status baseuri =
+class status uid baseuri =
object
- inherit GrafiteTypes.status baseuri
- inherit ApplyTransformation.status
+ inherit GrafiteTypes.status uid baseuri
+ inherit ApplyTransformation.status uid
end
exception TryingToAdd of string Lazy.t
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
(* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
- let status = new status baseuri in
+ (* FIXME: currently hardcoded to single user mode *)
+ let status = new status None baseuri in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri exn
-and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch mapath =
+and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid mapath =
let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
if List.mem fullmapath asserted then asserted,false
else
begin
let baseuri = NUri.uri_of_string baseuri in
let ngtime_of baseuri =
- let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+ let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
try
Some (Unix.stat ngpath).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
let asserted,to_be_compiled =
match ngtime with
Some ngtime ->
- let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+ let preamble = GrafiteTypes.Serializer.dependencies_of uid baseuri in
let asserted,children_bad =
List.fold_left
(fun (asserted,b) mapath ->
exception CircularDependency of string
class status:
- string ->
+ string option -> string ->
object
inherit GrafiteTypes.status
inherit ApplyTransformation.status
let similarsymbols_tag_name = "similarsymbolos" in
let similarsymbols_tag = `NAME similarsymbols_tag_name in
let initial_statuses current baseuri =
- let status = new MatitaEngine.status baseuri in
+(* FIXME : currently hard coded to single user mode *)
+ let status = new MatitaEngine.status None baseuri in
(match current with
Some current ->
NCicLibrary.time_travel status;
(status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
utf8_length parsed_text
-
-let status = ref (new MatitaEngine.status "cic:/matita");;
+(* FIXME: currently hard coded to single user mode *)
+let status = ref (new MatitaEngine.status (Some "ricciott") "cic:/matita");;
let history = ref [!status];;
let sequent_size = ref 40;;
; "open", retrieve ]
() in
MatitaInit.initialize_all ();
+ (* test begin *)
+ MatitaAuthentication.add_user "ricciott" "pippo123";
+ MatitaAuthentication.add_user "asperti" "pluto456";
+ (* test end *)
Netplex_main.startup
parallelizer
Netplex_log.logger_factories (* allow all built-in logging styles *)
projects / helm.git / commitdiff