1.1 --- a/src/Tools/isac/BaseDefinitions/check-unique.sml	Wed Apr 22 14:36:27 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml	Wed Apr 22 16:01:53 2020 +0200
     1.3 @@ -4,16 +4,19 @@
     1.4  
     1.5  Check entries to Know_Store unique.
     1.6  This is legacy code; check runs on #guh.
     1.7 +
     1.8 +"guh" stands for "globally unique handle" -- over all of the internet,
     1.9 +the last remaining code from Klaus Schmaranz's Dinopolis Project.
    1.10  *)
    1.11  signature CHECK_UNIQUE =
    1.12  sig
    1.13 -(*type switch *)
    1.14 -  type guh
    1.15 -(*val on *)
    1.16 -  val check_guhs_unique: bool Unsynchronized.ref
    1.17 +(*type guh *)
    1.18 +  type id
    1.19 +(*val check_guhs_unique *)
    1.20 +  val on: bool Unsynchronized.ref
    1.21  (*val collect *)
    1.22    val collect: ('a -> 'b) -> 'a Store.T -> 'b list;
    1.23 -  val message: ('a -> guh list) -> guh -> 'a -> unit;
    1.24 +  val message: ('a -> id list) -> id -> 'a -> unit;
    1.25  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.26    (*NONE*)
    1.27  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.28 @@ -26,16 +29,12 @@
    1.29  struct
    1.30  (**)
    1.31  
    1.32 -(*
    1.33 -  the last remaining code from Klaus Schmaranz's Dinopolis Project:
    1.34 -  guh stands for "globally unique handle" -- over all of the internet.
    1.35 -*)
    1.36 -type guh = string;
    1.37 +type id = string;
    1.38  
    1.39  (* switch for checking guhs unique before storing a pbl or met;
    1.40     set true at startup (done at begin of ROOT.ML)
    1.41     set false for editing Isac_Knowledge (done at end of ROOT.ML) *)
    1.42 -val check_guhs_unique = Unsynchronized.ref true;
    1.43 +val on = Unsynchronized.ref true;
    1.44  
    1.45  fun collect select_guh pbls =
    1.46    let
    1.47 @@ -45,9 +44,9 @@
    1.48        | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
    1.49    in nodes [] pbls end;
    1.50  
    1.51 -fun message select guh store =
    1.52 -  if member op = (select store) guh
    1.53 -  then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
    1.54 +fun message select id store =
    1.55 +  if member op = (select store) id
    1.56 +  then error ("Check_Unique failed with \"" ^ id ^ "\";\n" ^
    1.57  	      "use \"sort_guhs()\" for a list of guhs;\n" ^
    1.58  	      "consider setting \"Check_Unique.on := false\"")
    1.59    else ();