1.1 --- a/Admin/CHECKLIST	Sun Mar 01 16:22:37 2009 +0100
     1.2 +++ b/Admin/CHECKLIST	Sun Mar 01 16:48:06 2009 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  Checklist for official releases
     1.5  ===============================
     1.6  
     1.7 -- test alice, mosml, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0, x86-solaris, x86-cygwin;
     1.8 +- test mosml, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0, x86-solaris, x86-cygwin;
     1.9  
    1.10  - test ProofGeneral;
    1.11  

     2.1 --- a/etc/settings	Sun Mar 01 16:22:37 2009 +0100
     2.2 +++ b/etc/settings	Sun Mar 01 16:48:06 2009 +0100
     2.3 @@ -60,12 +60,6 @@
     2.4  #ML_OPTIONS=""
     2.5  #ML_PLATFORM=""
     2.6  
     2.7 -# Alice 1.4 (experimental!)
     2.8 -#ML_SYSTEM=alice
     2.9 -#ML_HOME="/usr/local/alice/bin"
    2.10 -#ML_OPTIONS=""
    2.11 -#ML_PLATFORM=""
    2.12 -
    2.13  
    2.14  ###
    2.15  ### JVM components (Scala or Java)

     3.1 --- a/src/Pure/IsaMakefile	Sun Mar 01 16:22:37 2009 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Sun Mar 01 16:48:06 2009 +0100
     3.3 @@ -19,14 +19,14 @@
     3.4  
     3.5  ## Pure
     3.6  
     3.7 -BOOTSTRAP_FILES = ML-Systems/alice.ML ML-Systems/exn.ML			\
     3.8 -  ML-Systems/ml_name_space.ML ML-Systems/mosml.ML			\
     3.9 -  ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
    3.10 -  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
    3.11 -  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
    3.12 -  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
    3.13 -  ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML		\
    3.14 -  ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML	\
    3.15 +BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML		\
    3.16 +  ML-Systems/mosml.ML ML-Systems/multithreading.ML			\
    3.17 +  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
    3.18 +  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
    3.19 +  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
    3.20 +  ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML		\
    3.21 +  ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
    3.22 +  ML-Systems/polyml_old_compiler4.ML					\
    3.23    ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
    3.24    ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
    3.25    ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML			\

     4.1 --- a/src/Pure/Isar/calculation.ML	Sun Mar 01 16:22:37 2009 +0100
     4.2 +++ b/src/Pure/Isar/calculation.ML	Sun Mar 01 16:48:06 2009 +0100
     4.3 @@ -15,7 +15,7 @@
     4.4    val symmetric: attribute
     4.5    val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
     4.6    val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
     4.7 -  val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
     4.8 +  val finally: (Facts.ref * Attrib.src list) list option -> bool ->
     4.9      Proof.state -> Proof.state Seq.seq
    4.10    val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    4.11    val moreover: bool -> Proof.state -> Proof.state
    4.12 @@ -150,7 +150,7 @@
    4.13  
    4.14  val also = calculate Proof.get_thmss false;
    4.15  val also_i = calculate (K I) false;
    4.16 -val finally_ = calculate Proof.get_thmss true;
    4.17 +val finally = calculate Proof.get_thmss true;
    4.18  val finally_i = calculate (K I) true;
    4.19  
    4.20  

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

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

     7.1 --- a/src/Pure/ML-Systems/alice.ML	Sun Mar 01 16:22:37 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,220 +0,0 @@
     7.4 -(*  Title:      Pure/ML-Systems/alice.ML
     7.5 -
     7.6 -Compatibility file for Alice 1.4.
     7.7 -
     7.8 -NOTE: there is no wrapper script; may run it interactively as follows:
     7.9 -
    7.10 -$ cd Isabelle/src/Pure
    7.11 -$ env ALICE_JIT_MODE=0 ISABELLE_HOME=$(cd ../..; pwd) alice
    7.12 -- val ml_system = "alice";
    7.13 -- use "ML-Systems/exn.ML";
    7.14 -- use "ML-Systems/universal.ML";
    7.15 -- use "ML-Systems/multithreading.ML";
    7.16 -- use "ML-Systems/time_limit.ML";
    7.17 -- use "ML-Systems/alice.ML";
    7.18 -- use "ROOT.ML";
    7.19 -- Session.finish ();
    7.20 -*)
    7.21 -
    7.22 -val ml_system_fix_ints = false;
    7.23 -
    7.24 -fun forget_structure _ = ();
    7.25 -
    7.26 -fun exit 0 = (OS.Process.exit OS.Process.success): unit
    7.27 -  | exit _ = OS.Process.exit OS.Process.failure;
    7.28 -
    7.29 -
    7.30 -(** ML system related **)
    7.31 -
    7.32 -(*low-level pointer equality*)
    7.33 -fun pointer_eq (_: 'a, _: 'a) = false;
    7.34 -
    7.35 -
    7.36 -(* integer compatibility -- downgraded IntInf *)
    7.37 -
    7.38 -structure Time =
    7.39 -struct
    7.40 -  open Time;
    7.41 -  val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
    7.42 -  val fromSeconds = Time.fromSeconds o IntInf.fromInt;
    7.43 -end;
    7.44 -
    7.45 -structure IntInf =
    7.46 -struct
    7.47 -  fun divMod (x, y) = (x div y, x mod y);
    7.48 -  open Int;
    7.49 -end;
    7.50 -
    7.51 -
    7.52 -(* restore old-style character / string functions *)
    7.53 -
    7.54 -exception Ord;
    7.55 -fun ord "" = raise Ord
    7.56 -  | ord s = Char.ord (String.sub (s, 0));
    7.57 -
    7.58 -val chr = String.str o chr;
    7.59 -val explode = map String.str o String.explode;
    7.60 -val implode = String.concat;
    7.61 -
    7.62 -
    7.63 -(* Poly/ML emulation *)
    7.64 -
    7.65 -fun quit () = exit 0;
    7.66 -
    7.67 -fun get_print_depth () = ! Print.depth;
    7.68 -fun print_depth n = Print.depth := n;
    7.69 -
    7.70 -
    7.71 -(* compiler-independent timing functions *)
    7.72 -
    7.73 -structure Timer =
    7.74 -struct
    7.75 -  open Timer;
    7.76 -  type cpu_timer = unit;
    7.77 -  fun startCPUTimer () = ();
    7.78 -  fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
    7.79 -  fun checkGCTime () = Time.zeroTime;
    7.80 -end;
    7.81 -
    7.82 -fun start_timing () =
    7.83 -  let val CPUtimer = Timer.startCPUTimer();
    7.84 -      val time = Timer.checkCPUTimer(CPUtimer)
    7.85 -  in  (CPUtimer,time)  end;
    7.86 -
    7.87 -fun end_timing (CPUtimer, {sys,usr}) =
    7.88 -  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    7.89 -      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    7.90 -  in  "User " ^ toString (usr2-usr) ^
    7.91 -      "  All "^ toString (sys2-sys + usr2-usr) ^
    7.92 -      " secs"
    7.93 -      handle Time => ""
    7.94 -  end;
    7.95 -
    7.96 -fun check_timer timer =
    7.97 -  let
    7.98 -    val {sys, usr} = Timer.checkCPUTimer timer;
    7.99 -    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
   7.100 -  in (sys, usr, gc) end;
   7.101 -
   7.102 -
   7.103 -(*prompts*)
   7.104 -fun ml_prompts p1 p2 = ();
   7.105 -
   7.106 -(*dummy implementation*)
   7.107 -fun profile (n: int) f x = f x;
   7.108 -
   7.109 -(*dummy implementation*)
   7.110 -fun exception_trace f = f ();
   7.111 -
   7.112 -(*dummy implementation*)
   7.113 -fun print x = x;
   7.114 -
   7.115 -
   7.116 -(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
   7.117 -
   7.118 -fun make_pp path pprint = (path, pprint);
   7.119 -fun install_pp (path, pp) = ();
   7.120 -
   7.121 -
   7.122 -(* ML command execution *)
   7.123 -
   7.124 -fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ());
   7.125 -fun use_file _ _ _ _ name = use name;
   7.126 -
   7.127 -
   7.128 -
   7.129 -(** interrupts **)
   7.130 -
   7.131 -exception Interrupt;
   7.132 -
   7.133 -fun interruptible f x = f x;
   7.134 -fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
   7.135 -
   7.136 -
   7.137 -(* basis library fixes *)
   7.138 -
   7.139 -structure TextIO =
   7.140 -struct
   7.141 -  open TextIO;
   7.142 -  fun inputLine is = TextIO.inputLine is
   7.143 -    handle IO.Io _ => raise Interrupt;
   7.144 -end;
   7.145 -
   7.146 -
   7.147 -
   7.148 -(** OS related **)
   7.149 -
   7.150 -structure OS =
   7.151 -struct
   7.152 -  open OS;
   7.153 -  structure FileSys =
   7.154 -  struct
   7.155 -    open FileSys;
   7.156 -    fun tmpName () =
   7.157 -      let val name = FileSys.tmpName () in
   7.158 -        if String.isSuffix "\000" name
   7.159 -        then String.substring (name, 0, size name - 1)
   7.160 -        else name
   7.161 -      end;
   7.162 -  end;
   7.163 -end;
   7.164 -
   7.165 -val cd = OS.FileSys.chDir;
   7.166 -val pwd = OS.FileSys.getDir;
   7.167 -
   7.168 -local
   7.169 -
   7.170 -fun read_file name =
   7.171 -  let val is = TextIO.openIn name
   7.172 -  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
   7.173 -
   7.174 -fun write_file name txt =
   7.175 -  let val os = TextIO.openOut name
   7.176 -  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
   7.177 -
   7.178 -in
   7.179 -
   7.180 -fun system_out script =
   7.181 -  let
   7.182 -    val script_name = OS.FileSys.tmpName ();
   7.183 -    val _ = write_file script_name script;
   7.184 -
   7.185 -    val output_name = OS.FileSys.tmpName ();
   7.186 -
   7.187 -    val status =
   7.188 -      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
   7.189 -        script_name ^ " /dev/null " ^ output_name);
   7.190 -    val rc = if OS.Process.isSuccess status then 0 else 1;
   7.191 -
   7.192 -    val output = read_file output_name handle IO.Io _ => "";
   7.193 -    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
   7.194 -    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   7.195 -  in (output, rc) end;
   7.196 -
   7.197 -end;
   7.198 -
   7.199 -structure OS =
   7.200 -struct
   7.201 -  open OS;
   7.202 -  structure FileSys =
   7.203 -  struct
   7.204 -    fun fileId name =
   7.205 -      (case system_out ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
   7.206 -        ("", _) => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
   7.207 -      | (s, _) => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
   7.208 -    val compare = Int.compare;
   7.209 -    fun fullPath name =
   7.210 -      (case system_out ("FILE='" ^ name ^
   7.211 -        "' && cd \"$(dirname \"$FILE\")\" && echo -n \"$(pwd -P)/$(basename \"$FILE\")\"") of
   7.212 -        ("", _) => raise SysErr ("Bad file", NONE)
   7.213 -      | (s, _) => s);
   7.214 -    open FileSys;
   7.215 -  end;
   7.216 -end;
   7.217 -
   7.218 -fun process_id () = raise Fail "process_id undefined";
   7.219 -
   7.220 -fun getenv var =
   7.221 -  (case OS.Process.getEnv var of
   7.222 -    NONE => ""
   7.223 -  | SOME txt => txt);

     8.1 --- a/src/Pure/Syntax/parser.ML	Sun Mar 01 16:22:37 2009 +0100
     8.2 +++ b/src/Pure/Syntax/parser.ML	Sun Mar 01 16:48:06 2009 +0100
     8.3 @@ -73,10 +73,10 @@
     8.4        val chain_from = case (pri, rhs) of (~1, [Nonterminal (id, ~1)]) => SOME id | _ => NONE;
     8.5  
     8.6        (*store chain if it does not already exist*)
     8.7 -      val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from_ =>
     8.8 -        let val old_tos = these (AList.lookup (op =) chains from_) in
     8.9 +      val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
    8.10 +        let val old_tos = these (AList.lookup (op =) chains from) in
    8.11            if member (op =) old_tos lhs then (NONE, chains)
    8.12 -          else (SOME from_, AList.update (op =) (from_, insert (op =) lhs old_tos) chains)
    8.13 +          else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains)
    8.14          end;
    8.15  
    8.16        (*propagate new chain in lookahead and lambda lists;
    8.17 @@ -410,7 +410,7 @@
    8.18  
    8.19      fun pretty_nt (name, tag) =
    8.20        let
    8.21 -        fun prod_of_chain from_ = ([Nonterminal (from_, ~1)], "", ~1);
    8.22 +        fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
    8.23  
    8.24          val nt_prods =
    8.25            Library.foldl (gen_union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
    8.26 @@ -552,8 +552,8 @@
    8.27            val to_tag = convert_tag to;
    8.28  
    8.29            fun make [] result = result
    8.30 -            | make (from_ :: froms) result = make froms ((to_tag,
    8.31 -                ([Nonterminal (convert_tag from_, ~1)], "", ~1)) :: result);
    8.32 +            | make (from :: froms) result = make froms ((to_tag,
    8.33 +                ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
    8.34          in mk_chain_prods cs (make froms [] @ result) end;
    8.35  
    8.36      val chain_prods = mk_chain_prods chains2 [];

     9.1 --- a/src/Pure/Syntax/syn_ext.ML	Sun Mar 01 16:22:37 2009 +0100
     9.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sun Mar 01 16:48:06 2009 +0100
     9.3 @@ -26,7 +26,7 @@
     9.4    val logic: string
     9.5    val args: string
     9.6    val cargs: string
     9.7 -  val any_: string
     9.8 +  val any: string
     9.9    val sprop: string
    9.10    val typ_to_nonterm: typ -> string
    9.11    datatype xsymb =
    9.12 @@ -108,8 +108,8 @@
    9.13  val sprop = "#prop";
    9.14  val spropT = Type (sprop, []);
    9.15  
    9.16 -val any_ = "any";
    9.17 -val anyT = Type (any_, []);
    9.18 +val any = "any";
    9.19 +val anyT = Type (any, []);
    9.20  
    9.21  
    9.22  
    9.23 @@ -181,7 +181,7 @@
    9.24    | typ_to_nt default _ = default;
    9.25  
    9.26  (*get nonterminal for rhs*)
    9.27 -val typ_to_nonterm = typ_to_nt any_;
    9.28 +val typ_to_nonterm = typ_to_nt any;
    9.29  
    9.30  (*get nonterminal for lhs*)
    9.31  val typ_to_nonterm1 = typ_to_nt logic;

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