--- a/NEWS Tue Jan 05 11:25:01 2010 +0100
+++ b/NEWS Tue Jan 05 11:25:14 2010 +0100
@@ -47,6 +47,11 @@
* Subgoal.FOCUS (and variants): resulting goal state is normalized as
usual for resolution. Rare INCOMPATIBILITY.
+* Discontinued old TheoryDataFun with its copy/init operation -- data
+needs to be pure. Functor Theory_Data_PP retains the traditional
+Pretty.pp argument to merge, which is absent in the standard
+Theory_Data version.
+
*** System ***
@@ -54,6 +59,10 @@
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that
proof terms are enabled unconditionally in the new HOL-Proofs image.
+* Discontinued old ISABELLE and ISATOOL environment settings (legacy
+feature since Isabelle2009). Use ISABELLE_PROCESS and ISABELLE_TOOL,
+respectively.
+
New in Isabelle2009-1 (December 2009)
--- a/lib/scripts/getsettings Tue Jan 05 11:25:01 2010 +0100
+++ b/lib/scripts/getsettings Tue Jan 05 11:25:14 2010 +0100
@@ -21,9 +21,11 @@
#key executables
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-#legacy settings
-ISABELLE="$ISABELLE_PROCESS"
-ISATOOL="$ISABELLE_TOOL"
+
+function isabelle ()
+{
+ "$ISABELLE_TOOL" "$@"
+}
#Isabelle distribution identifier -- filled in automatically!
ISABELLE_IDENTIFIER=""
--- a/src/Pure/Concurrent/future.scala Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/Concurrent/future.scala Tue Jan 05 11:25:14 2010 +0100
@@ -21,6 +21,7 @@
{
def value[A](x: A): Future[A] = new Finished_Future(x)
def fork[A](body: => A): Future[A] = new Pending_Future(body)
+ def promise[A]: Promise[A] = new Promise_Future
}
abstract class Future[A]
@@ -38,6 +39,11 @@
}
}
+abstract class Promise[A] extends Future[A]
+{
+ def fulfill(x: A): Unit
+}
+
private class Finished_Future[A](x: A) extends Future[A]
{
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
@@ -64,4 +70,37 @@
}
}
+private class Promise_Future[A] extends Promise[A]
+{
+ @volatile private var result: Option[A] = None
+ private case object Read
+ private case class Write(x: A)
+
+ private val receiver = actor {
+ loop {
+ react {
+ case Read if result.isDefined => reply(result.get)
+ case Write(x) =>
+ if (result.isDefined) reply(false)
+ else { result = Some(x); reply(true) }
+ }
+ }
+ }
+
+ def peek: Option[Exn.Result[A]] = result.map(Exn.Res(_))
+
+ def join: A =
+ result match {
+ case Some(res) => res
+ case None => (receiver !? Read).asInstanceOf[A]
+ }
+
+ def fulfill(x: A) {
+ receiver !? Write(x) match {
+ case false => error("Duplicate fulfillment of promise")
+ case _ =>
+ }
+ }
+}
+
--- a/src/Pure/General/markup.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/General/markup.ML Tue Jan 05 11:25:14 2010 +0100
@@ -105,6 +105,7 @@
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
+ val assignN: string val assign: T
val editN: string val edit: string -> string -> T
val pidN: string
val promptN: string val prompt: T
@@ -305,6 +306,8 @@
(* interactive documents *)
+val (assignN, assign) = markup_elem "assign";
+
val editN = "edit";
fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
--- a/src/Pure/General/markup.scala Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/General/markup.scala Tue Jan 05 11:25:14 2010 +0100
@@ -153,6 +153,7 @@
/* interactive documents */
+ val ASSIGN = "assign"
val EDIT = "edit"
--- a/src/Pure/IsaMakefile Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/IsaMakefile Tue Jan 05 11:25:14 2010 +0100
@@ -143,7 +143,6 @@
$(FULL_JAR): $(SCALA_FILES)
@rm -rf classes && mkdir classes
"$(SCALA_HOME)/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
- "$(SCALA_HOME)/bin/scaladoc" -d classes $(SCALA_FILES)
@cp $(SCALA_FILES) classes/isabelle
@mkdir -p "$(JAR_DIR)"
@cd classes; jar cfe `jvmpath "$(PURE_JAR)"` isabelle.GUI_Setup isabelle
--- a/src/Pure/Isar/isar_document.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/Isar/isar_document.ML Tue Jan 05 11:25:14 2010 +0100
@@ -234,8 +234,9 @@
fun report_updates [] = ()
| report_updates updates =
- Output.status
- (implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates));
+ implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
+ |> Markup.markup Markup.assign
+ |> Output.status;
in
--- a/src/Pure/Isar/outer_keyword.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/Isar/outer_keyword.ML Tue Jan 05 11:25:14 2010 +0100
@@ -43,6 +43,7 @@
val dest_commands: unit -> string list
val command_keyword: string -> T option
val command_tags: string -> string list
+ val keyword_status_reportN: string
val report: unit -> unit
val keyword: string -> unit
val command: string -> T -> unit
@@ -142,33 +143,38 @@
(* report *)
+val keyword_status_reportN = "keyword_status_report";
+
+fun report_message s =
+ (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
+
fun report_keyword name =
- Pretty.mark (Markup.keyword_decl name)
- (Pretty.str ("Outer syntax keyword: " ^ quote name));
+ report_message (Markup.markup (Markup.keyword_decl name)
+ ("Outer syntax keyword: " ^ quote name));
fun report_command (name, kind) =
- Pretty.mark (Markup.command_decl name (kind_of kind))
- (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
-
-fun status_writeln s = (Output.status s; writeln s);
+ report_message (Markup.markup (Markup.command_decl name (kind_of kind))
+ ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
fun report () =
let val (keywords, commands) = CRITICAL (fn () =>
(dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
- in map report_keyword keywords @ map report_command commands end
- |> Pretty.chunks |> Pretty.string_of |> status_writeln;
+ in
+ List.app report_keyword keywords;
+ List.app report_command commands
+ end;
(* augment tables *)
fun keyword name =
(change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
- status_writeln (Pretty.string_of (report_keyword name)));
+ report_keyword name);
fun command name kind =
(change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
change_commands (Symtab.update (name, kind));
- status_writeln (Pretty.string_of (report_command (name, kind))));
+ report_command (name, kind));
(* command categories *)
--- a/src/Pure/Isar/proof.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/Isar/proof.ML Tue Jan 05 11:25:14 2010 +0100
@@ -862,14 +862,10 @@
val results =
tl (conclude_goal goal_ctxt goal stmt)
|> burrow (ProofContext.export goal_ctxt outer_ctxt);
-
- val (after_local, after_global) = after_qed;
- fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
- fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
in
outer_state
|> map_context (after_ctxt props)
- |> pair ((after_local', after_global'), results)
+ |> pair (after_qed, results)
end;
end;
--- a/src/Pure/System/cygwin.scala Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/System/cygwin.scala Tue Jan 05 11:25:14 2010 +0100
@@ -104,7 +104,7 @@
def setup(parent: Component, root: File)
{
- if (!root.mkdirs) error("Failed to create root directory: " + root)
+ if (!root.isDirectory && !root.mkdirs) error("Failed to create root directory: " + root)
val download = new File(root, "download")
if (!download.mkdir) error("Failed to create download directory: " + download)
@@ -114,10 +114,9 @@
try { Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe) }
catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
- val (_, rc) = Standard_System.process_output(
- Standard_System.raw_execute(root, null, true,
- setup_exe.toString, "-R", root.toString, "-l", download.toString,
- "-P", "perl,python", "-q", "-n"))
+ val (_, rc) = Standard_System.raw_exec(root, null, true,
+ setup_exe.toString, "-R", root.toString, "-l", download.toString,
+ "-P", "make,perl,python", "-q", "-n")
if (rc != 0) error("Cygwin setup failed!")
sanity_check(root)
--- a/src/Pure/System/isabelle_process.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/System/isabelle_process.ML Tue Jan 05 11:25:14 2010 +0100
@@ -88,7 +88,8 @@
(* init *)
fun init out =
- (Unsynchronized.change print_mode (update (op =) isabelle_processN);
+ (Unsynchronized.change print_mode
+ (fold (update (op =)) [isabelle_processN, OuterKeyword.keyword_status_reportN]);
setup_channels out |> init_message;
OuterKeyword.report ();
Output.status (Markup.markup Markup.ready "");
--- a/src/Pure/System/isabelle_system.scala Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Jan 05 11:25:14 2010 +0100
@@ -42,8 +42,7 @@
if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
val cmdline =
shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
- val (output, rc) =
- Standard_System.process_output(Standard_System.raw_execute(null, env0, true, cmdline: _*))
+ val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
if (rc != 0) error(output)
val entries =
--- a/src/Pure/System/standard_system.scala Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/System/standard_system.scala Tue Jan 05 11:25:14 2010 +0100
@@ -132,6 +132,9 @@
}
(output, rc)
}
+
+ def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*):
+ (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
}
--- a/src/Pure/Thy/thy_info.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Jan 05 11:25:14 2010 +0100
@@ -389,14 +389,16 @@
val futures = fold fork tasks Symtab.empty;
- val exns = tasks |> maps (fn (name, _) =>
+ val failed = tasks |> maps (fn (name, _) =>
let
val after_load = Future.join (the (Symtab.lookup futures name));
val _ = join_thy name;
val _ = after_load ();
- in [] end handle exn => (kill_thy name; [exn]));
+ in [] end handle exn => [(name, exn)]) |> rev;
- in ignore (Exn.release_all (map Exn.Exn (rev exns))) end) ();
+ val _ = List.app (kill_thy o #1) failed;
+ val _ = Exn.release_all (map (Exn.Exn o #2) failed);
+ in () end) ();
fun schedule_seq tasks =
Graph.topological_order tasks
--- a/src/Pure/axclass.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/axclass.ML Tue Jan 05 11:25:14 2010 +0100
@@ -114,7 +114,7 @@
(* setup data *)
-structure AxClassData = TheoryDataFun
+structure AxClassData = Theory_Data_PP
(
type T = axclasses * (instances * inst_params);
val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
--- a/src/Pure/context.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/context.ML Tue Jan 05 11:25:14 2010 +0100
@@ -426,9 +426,9 @@
val declare = declare_theory_data;
fun get k dest thy =
- dest (case Datatab.lookup (data_of thy) k of
+ (case Datatab.lookup (data_of thy) k of
SOME x => x
- | NONE => invoke_empty k); (*adhoc value*)
+ | NONE => invoke_empty k) |> dest;
fun put k mk x = modify_thy (Datatab.update (k, mk x));
@@ -574,7 +574,7 @@
(** theory data **)
-signature OLD_THEORY_DATA_ARGS =
+signature THEORY_DATA_PP_ARGS =
sig
type T
val empty: T
@@ -582,34 +582,6 @@
val merge: Pretty.pp -> T * T -> T
end;
-signature OLD_THEORY_DATA =
-sig
- type T
- val get: theory -> T
- val put: T -> theory -> theory
- val map: (T -> T) -> theory -> theory
- val init: theory -> theory
-end;
-
-functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): OLD_THEORY_DATA =
-struct
-
-type T = Data.T;
-exception Data of T;
-
-val kind = Context.Theory_Data.declare
- (Data Data.empty)
- (fn Data x => Data (Data.extend x))
- (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
-
-val get = Context.Theory_Data.get kind (fn Data x => x);
-val put = Context.Theory_Data.put kind Data;
-fun map f thy = put (f (get thy)) thy;
-
-fun init thy = map I thy;
-
-end;
-
signature THEORY_DATA_ARGS =
sig
type T
@@ -626,21 +598,32 @@
val map: (T -> T) -> theory -> theory
end;
-functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
+functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
struct
-structure Result = TheoryDataFun
-(
- type T = Data.T;
- val empty = Data.empty;
- val extend = Data.extend;
- fun merge _ = Data.merge;
-);
+type T = Data.T;
+exception Data of T;
-open Result;
+val kind = Context.Theory_Data.declare
+ (Data Data.empty)
+ (fn Data x => Data (Data.extend x))
+ (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
+
+val get = Context.Theory_Data.get kind (fn Data x => x);
+val put = Context.Theory_Data.put kind Data;
+fun map f thy = put (f (get thy)) thy;
end;
+functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
+ Theory_Data_PP
+ (
+ type T = Data.T;
+ val empty = Data.empty;
+ val extend = Data.extend;
+ fun merge _ = Data.merge;
+ );
+
(** proof data **)
--- a/src/Pure/sign.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/sign.ML Tue Jan 05 11:25:14 2010 +0100
@@ -148,7 +148,7 @@
fun make_sign (naming, syn, tsig, consts) =
Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
-structure SignData = TheoryDataFun
+structure SignData = Theory_Data_PP
(
type T = sign;
fun extend (Sign {syn, tsig, consts, ...}) =
--- a/src/Pure/theory.ML Tue Jan 05 11:25:01 2010 +0100
+++ b/src/Pure/theory.ML Tue Jan 05 11:25:14 2010 +0100
@@ -86,7 +86,7 @@
fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
-structure ThyData = TheoryDataFun
+structure ThyData = Theory_Data_PP
(
type T = thy;
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;