# HG changeset patch # User wenzelm # Date 1235922486 -3600 # Node ID 3633f560f4c3e3458ebb9ca9950591c26af3d628 # Parent 82144a95f9ec8bcdeda4dc7929d19a89318b382d discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway; diff -r 82144a95f9ec -r 3633f560f4c3 Admin/CHECKLIST --- 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; diff -r 82144a95f9ec -r 3633f560f4c3 etc/settings --- 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) diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/IsaMakefile --- 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 \ diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/Isar/calculation.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; diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/Isar/expression.ML --- 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 diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/Isar/isar_syn.ML --- 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" diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/ML-Systems/alice.ML --- 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); diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/Syntax/parser.ML --- 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 []; diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/Syntax/syn_ext.ML --- 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; diff -r 82144a95f9ec -r 3633f560f4c3 src/Pure/Syntax/syntax.ML --- 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"]);