# HG changeset patch
# User wenzelm
# Date 1262630686 -3600
# Node ID b589bbbdb1b6e3efcce773d191e990e7b15c46b0
# Parent  cd642bb91f64fe910e16e55a0f6a57444518d42b# Parent  8821e329370270984b6db5e2b74f3351c8e9bd69
merged

diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/Concurrent/future.scala	Mon Jan 04 19:44:46 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 _ =>
+    }
+  }
+}
+
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/General/markup.ML	Mon Jan 04 19:44:46 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)]);
 
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/General/markup.scala	Mon Jan 04 19:44:46 2010 +0100
@@ -153,6 +153,7 @@
 
   /* interactive documents */
 
+  val ASSIGN = "assign"
   val EDIT = "edit"
 
 
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/IsaMakefile	Mon Jan 04 19:44:46 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
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/Isar/isar_document.ML	Mon Jan 04 19:44:46 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
 
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Mon Jan 04 19:44:46 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 *)
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 04 19:44:46 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;
diff -r cd642bb91f64 -r b589bbbdb1b6 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Jan 04 16:00:24 2010 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Jan 04 19:44:46 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 "");