discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;

--- a/Admin/CHECKLIST	Sun Mar 01 16:22:37 2009 +0100
+++ b/Admin/CHECKLIST	Sun Mar 01 16:48:06 2009 +0100
@@ -1,7 +1,7 @@
 Checklist for official releases
 ===============================
 
-- test alice, mosml, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0, x86-solaris, x86-cygwin;
+- test mosml, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0, x86-solaris, x86-cygwin;
 
 - test ProofGeneral;
 

--- a/etc/settings	Sun Mar 01 16:22:37 2009 +0100
+++ b/etc/settings	Sun Mar 01 16:48:06 2009 +0100
@@ -60,12 +60,6 @@
 #ML_OPTIONS=""
 #ML_PLATFORM=""
 
-# Alice 1.4 (experimental!)
-#ML_SYSTEM=alice
-#ML_HOME="/usr/local/alice/bin"
-#ML_OPTIONS=""
-#ML_PLATFORM=""
-
 
 ###
 ### JVM components (Scala or Java)

--- a/src/Pure/IsaMakefile	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/IsaMakefile	Sun Mar 01 16:48:06 2009 +0100
@@ -19,14 +19,14 @@
 
 ## Pure
 
-BOOTSTRAP_FILES = ML-Systems/alice.ML ML-Systems/exn.ML			\
-  ML-Systems/ml_name_space.ML ML-Systems/mosml.ML			\
-  ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
-  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
-  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
-  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
-  ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML		\
-  ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML	\
+BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML		\
+  ML-Systems/mosml.ML ML-Systems/multithreading.ML			\
+  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
+  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
+  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
+  ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML		\
+  ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
+  ML-Systems/polyml_old_compiler4.ML					\
   ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
   ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
   ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML			\

--- a/src/Pure/Isar/calculation.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -15,7 +15,7 @@
   val symmetric: attribute
   val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
+  val finally: (Facts.ref * Attrib.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.seq
   val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
@@ -150,7 +150,7 @@
 
 val also = calculate Proof.get_thmss false;
 val also_i = calculate (K I) false;
-val finally_ = calculate Proof.get_thmss true;
+val finally = calculate Proof.get_thmss true;
 val finally_i = calculate (K I) true;
 
 

--- a/src/Pure/Isar/expression.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -726,14 +726,14 @@
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
-    bname raw_predicate_bname raw_imprt raw_body thy =
+    bname raw_predicate_bname raw_import raw_body thy =
   let
     val name = Sign.full_bname thy bname;
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
     val ((fixed, deps, body_elems), (parms, ctxt')) =
-      prep_decl raw_imprt I raw_body (ProofContext.init thy);
+      prep_decl raw_import I raw_body (ProofContext.init thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
     val predicate_bname = if raw_predicate_bname = "" then bname

--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -693,7 +693,7 @@
 val _ =
   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
     (K.tag_proof K.prf_chain)
-    (calc_args >> (Toplevel.proofs' o Calculation.finally_));
+    (calc_args >> (Toplevel.proofs' o Calculation.finally));
 
 val _ =
   OuterSyntax.command "moreover" "augment calculation by current facts"

--- a/src/Pure/ML-Systems/alice.ML	Sun Mar 01 16:22:37 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,220 +0,0 @@
-(*  Title:      Pure/ML-Systems/alice.ML
-
-Compatibility file for Alice 1.4.
-
-NOTE: there is no wrapper script; may run it interactively as follows:
-
-$ cd Isabelle/src/Pure
-$ env ALICE_JIT_MODE=0 ISABELLE_HOME=$(cd ../..; pwd) alice
-- val ml_system = "alice";
-- use "ML-Systems/exn.ML";
-- use "ML-Systems/universal.ML";
-- use "ML-Systems/multithreading.ML";
-- use "ML-Systems/time_limit.ML";
-- use "ML-Systems/alice.ML";
-- use "ROOT.ML";
-- Session.finish ();
-*)
-
-val ml_system_fix_ints = false;
-
-fun forget_structure _ = ();
-
-fun exit 0 = (OS.Process.exit OS.Process.success): unit
-  | exit _ = OS.Process.exit OS.Process.failure;
-
-
-(** ML system related **)
-
-(*low-level pointer equality*)
-fun pointer_eq (_: 'a, _: 'a) = false;
-
-
-(* integer compatibility -- downgraded IntInf *)
-
-structure Time =
-struct
-  open Time;
-  val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
-  val fromSeconds = Time.fromSeconds o IntInf.fromInt;
-end;
-
-structure IntInf =
-struct
-  fun divMod (x, y) = (x div y, x mod y);
-  open Int;
-end;
-
-
-(* restore old-style character / string functions *)
-
-exception Ord;
-fun ord "" = raise Ord
-  | ord s = Char.ord (String.sub (s, 0));
-
-val chr = String.str o chr;
-val explode = map String.str o String.explode;
-val implode = String.concat;
-
-
-(* Poly/ML emulation *)
-
-fun quit () = exit 0;
-
-fun get_print_depth () = ! Print.depth;
-fun print_depth n = Print.depth := n;
-
-
-(* compiler-independent timing functions *)
-
-structure Timer =
-struct
-  open Timer;
-  type cpu_timer = unit;
-  fun startCPUTimer () = ();
-  fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
-  fun checkGCTime () = Time.zeroTime;
-end;
-
-fun start_timing () =
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
-
-fun end_timing (CPUtimer, {sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  All "^ toString (sys2-sys + usr2-usr) ^
-      " secs"
-      handle Time => ""
-  end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
-
-
-(*prompts*)
-fun ml_prompts p1 p2 = ();
-
-(*dummy implementation*)
-fun profile (n: int) f x = f x;
-
-(*dummy implementation*)
-fun exception_trace f = f ();
-
-(*dummy implementation*)
-fun print x = x;
-
-
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
-
-fun make_pp path pprint = (path, pprint);
-fun install_pp (path, pp) = ();
-
-
-(* ML command execution *)
-
-fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ());
-fun use_file _ _ _ _ name = use name;
-
-
-
-(** interrupts **)
-
-exception Interrupt;
-
-fun interruptible f x = f x;
-fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
-
-
-(* basis library fixes *)
-
-structure TextIO =
-struct
-  open TextIO;
-  fun inputLine is = TextIO.inputLine is
-    handle IO.Io _ => raise Interrupt;
-end;
-
-
-
-(** OS related **)
-
-structure OS =
-struct
-  open OS;
-  structure FileSys =
-  struct
-    open FileSys;
-    fun tmpName () =
-      let val name = FileSys.tmpName () in
-        if String.isSuffix "\000" name
-        then String.substring (name, 0, size name - 1)
-        else name
-      end;
-  end;
-end;
-
-val cd = OS.FileSys.chDir;
-val pwd = OS.FileSys.getDir;
-
-local
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
-fun system_out script =
-  let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val output_name = OS.FileSys.tmpName ();
-
-    val status =
-      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
-        script_name ^ " /dev/null " ^ output_name);
-    val rc = if OS.Process.isSuccess status then 0 else 1;
-
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-  in (output, rc) end;
-
-end;
-
-structure OS =
-struct
-  open OS;
-  structure FileSys =
-  struct
-    fun fileId name =
-      (case system_out ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
-        ("", _) => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
-      | (s, _) => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
-    val compare = Int.compare;
-    fun fullPath name =
-      (case system_out ("FILE='" ^ name ^
-        "' && cd \"$(dirname \"$FILE\")\" && echo -n \"$(pwd -P)/$(basename \"$FILE\")\"") of
-        ("", _) => raise SysErr ("Bad file", NONE)
-      | (s, _) => s);
-    open FileSys;
-  end;
-end;
-
-fun process_id () = raise Fail "process_id undefined";
-
-fun getenv var =
-  (case OS.Process.getEnv var of
-    NONE => ""
-  | SOME txt => txt);

--- a/src/Pure/Syntax/parser.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Syntax/parser.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -73,10 +73,10 @@
       val chain_from = case (pri, rhs) of (~1, [Nonterminal (id, ~1)]) => SOME id | _ => NONE;
 
       (*store chain if it does not already exist*)
-      val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from_ =>
-        let val old_tos = these (AList.lookup (op =) chains from_) in
+      val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
+        let val old_tos = these (AList.lookup (op =) chains from) in
           if member (op =) old_tos lhs then (NONE, chains)
-          else (SOME from_, AList.update (op =) (from_, insert (op =) lhs old_tos) chains)
+          else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains)
         end;
 
       (*propagate new chain in lookahead and lambda lists;
@@ -410,7 +410,7 @@
 
     fun pretty_nt (name, tag) =
       let
-        fun prod_of_chain from_ = ([Nonterminal (from_, ~1)], "", ~1);
+        fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
 
         val nt_prods =
           Library.foldl (gen_union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
@@ -552,8 +552,8 @@
           val to_tag = convert_tag to;
 
           fun make [] result = result
-            | make (from_ :: froms) result = make froms ((to_tag,
-                ([Nonterminal (convert_tag from_, ~1)], "", ~1)) :: result);
+            | make (from :: froms) result = make froms ((to_tag,
+                ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
         in mk_chain_prods cs (make froms [] @ result) end;
 
     val chain_prods = mk_chain_prods chains2 [];

--- a/src/Pure/Syntax/syn_ext.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -26,7 +26,7 @@
   val logic: string
   val args: string
   val cargs: string
-  val any_: string
+  val any: string
   val sprop: string
   val typ_to_nonterm: typ -> string
   datatype xsymb =
@@ -108,8 +108,8 @@
 val sprop = "#prop";
 val spropT = Type (sprop, []);
 
-val any_ = "any";
-val anyT = Type (any_, []);
+val any = "any";
+val anyT = Type (any, []);
 
 
 
@@ -181,7 +181,7 @@
   | typ_to_nt default _ = default;
 
 (*get nonterminal for rhs*)
-val typ_to_nonterm = typ_to_nt any_;
+val typ_to_nonterm = typ_to_nt any;
 
 (*get nonterminal for lhs*)
 val typ_to_nonterm1 = typ_to_nt logic;

--- a/src/Pure/Syntax/syntax.ML	Sun Mar 01 16:22:37 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Mar 01 16:48:06 2009 +0100
@@ -390,7 +390,7 @@
 val basic_nonterms =
   (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
     SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
-    "asms", SynExt.any_, SynExt.sprop, "num_const", "float_const",
+    "asms", SynExt.any, SynExt.sprop, "num_const", "float_const",
     "index", "struct"]);