# HG changeset patch
# User wenzelm
# Date 1310419240 -7200
# Node ID 24b8244d672bf6e4809f120b14ac49ca87787d1c
# Parent  366d5726de0962dbc3ba44f2c5e33a76263560b0# Parent  ab11dcfa3e6d3e4829425c39310a46b617616a9c
merged

diff -r 366d5726de09 -r 24b8244d672b src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -117,7 +117,7 @@
     val ok =
       (case the (Single_Assignment.peek result) of
         Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
-      | Exn.Result _ => true);
+      | Exn.Res _ => true);
   in ok end;
 
 
@@ -482,7 +482,7 @@
     val task = Task_Queue.dummy_task ();
     val group = Task_Queue.group_of_task task;
     val result = Single_Assignment.var "value" : 'a result;
-    val _ = assign_result group result (Exn.Result x);
+    val _ = assign_result group result (Exn.Res x);
   in Future {promised = false, task = task, result = result} end;
 
 fun map_future f x =
@@ -544,7 +544,7 @@
         else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
     in () end;
 
-fun fulfill x res = fulfill_result x (Exn.Result res);
+fun fulfill x res = fulfill_result x (Exn.Res res);
 
 
 (* cancellation *)
diff -r 366d5726de09 -r 24b8244d672b src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -23,7 +23,7 @@
   | Result res => SOME res);
 
 fun lazy e = Lazy (Unsynchronized.ref (Expr e));
-fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
 
 
 (* force result *)
diff -r 366d5726de09 -r 24b8244d672b src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -38,7 +38,7 @@
         (case peek v of
           NONE =>
             (case Multithreading.sync_wait NONE NONE cond lock of
-              Exn.Result _ => wait ()
+              Exn.Res _ => wait ()
             | Exn.Exn exn => reraise exn)
         | SOME x => x);
     in wait () end);
diff -r 366d5726de09 -r 24b8244d672b src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -47,8 +47,8 @@
           (case f x of
             NONE =>
               (case Multithreading.sync_wait NONE (time_limit x) cond lock of
-                Exn.Result true => try_change ()
-              | Exn.Result false => NONE
+                Exn.Res true => try_change ()
+              | Exn.Res false => NONE
               | Exn.Exn exn => reraise exn)
           | SOME (y, x') =>
               uninterruptible (fn _ => fn () =>
diff -r 366d5726de09 -r 24b8244d672b src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/General/exn.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -1,13 +1,13 @@
 (*  Title:      Pure/General/exn.ML
     Author:     Makarius
 
-Extra support for exceptions.
+Support for exceptions.
 *)
 
 signature EXN =
 sig
-  datatype 'a result = Result of 'a | Exn of exn
-  val get_result: 'a result -> 'a option
+  datatype 'a result = Res of 'a | Exn of exn
+  val get_res: 'a result -> 'a option
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
@@ -33,24 +33,24 @@
 (* runtime exceptions as values *)
 
 datatype 'a result =
-  Result of 'a |
+  Res of 'a |
   Exn of exn;
 
-fun get_result (Result x) = SOME x
-  | get_result _ = NONE;
+fun get_res (Res x) = SOME x
+  | get_res _ = NONE;
 
 fun get_exn (Exn exn) = SOME exn
   | get_exn _ = NONE;
 
-fun capture f x = Result (f x) handle e => Exn e;
+fun capture f x = Res (f x) handle e => Exn e;
 
-fun release (Result y) = y
+fun release (Res y) = y
   | release (Exn e) = reraise e;
 
-fun flat_result (Result x) = x
+fun flat_result (Res x) = x
   | flat_result (Exn e) = Exn e;
 
-fun map_result f (Result x) = Result (f x)
+fun map_result f (Res x) = Res (f x)
   | map_result f (Exn e) = Exn e;
 
 fun maps_result f = flat_result o map_result f;
@@ -72,7 +72,7 @@
   | is_interrupt_exn _ = false;
 
 fun interruptible_capture f x =
-  Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
+  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
 (* nested exceptions *)
@@ -84,8 +84,8 @@
 and flatten_list exns = List.concat (map flatten exns);
 
 fun release_all results =
-  if List.all (fn Result _ => true | _ => false) results
-  then map (fn Result x => x) results
+  if List.all (fn Res _ => true | _ => false) results
+  then map (fn Res x => x) results
   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
 
 fun release_first results = release_all results
diff -r 366d5726de09 -r 24b8244d672b src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/General/exn.scala	Mon Jul 11 23:20:40 2011 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/exn.scala
     Author:     Makarius
 
-Extra support for exceptions (arbitrary throwables).
+Support for exceptions (arbitrary throwables).
 */
 
 package isabelle
@@ -12,8 +12,8 @@
   /* runtime exceptions as values */
 
   sealed abstract class Result[A]
-  case class Res[A](val result: A) extends Result[A]
-  case class Exn[A](val exn: Throwable) extends Result[A]
+  case class Res[A](res: A) extends Result[A]
+  case class Exn[A](exn: Throwable) extends Result[A]
 
   def capture[A](e: => A): Result[A] =
     try { Res(e) }
diff -r 366d5726de09 -r 24b8244d672b src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -96,9 +96,8 @@
   val prompt_fn = Unsynchronized.ref raw_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
-  val raw_message_fn =
-    Unsynchronized.ref
-      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
+  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
diff -r 366d5726de09 -r 24b8244d672b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -1008,8 +1008,8 @@
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     |> int ? (fn goal_state =>
       (case test_proof goal_state of
-        Exn.Result (SOME _) => goal_state
-      | Exn.Result NONE => error (fail_msg (context_of goal_state))
+        Exn.Res (SOME _) => goal_state
+      | Exn.Res NONE => error (fail_msg (context_of goal_state))
       | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   end;
 
diff -r 366d5726de09 -r 24b8244d672b src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -101,7 +101,7 @@
 fun debugging f x =
   if ! debug then
     Exn.release (exception_trace (fn () =>
-      Exn.Result (f x) handle
+      Exn.Res (f x) handle
         exn as UNDEF => Exn.Exn exn
       | exn as EXCURSION_FAIL _ => Exn.Exn exn))
   else f x;
diff -r 366d5726de09 -r 24b8244d672b src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -55,7 +55,7 @@
 
 fun with_attributes _ e = e [];
 
-fun sync_wait _ _ _ _ = Exn.Result true;
+fun sync_wait _ _ _ _ = Exn.Res true;
 
 
 (* tracing *)
diff -r 366d5726de09 -r 24b8244d672b src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -97,8 +97,8 @@
     (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
     (fn _ =>
       (case time of
-        SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
-      | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
+        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
+      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
       handle exn => Exn.Exn exn);
 
 
diff -r 366d5726de09 -r 24b8244d672b src/Pure/ML/install_pp_polyml-5.3.ML
--- a/src/Pure/ML/install_pp_polyml-5.3.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -14,13 +14,13 @@
   (case Future.peek x of
     NONE => PolyML.PrettyString "<future>"
   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth)));
+  | SOME (Exn.Res y) => pretty (y, depth)));
 
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Lazy.peek x of
     NONE => PolyML.PrettyString "<lazy>"
   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth)));
+  | SOME (Exn.Res y) => pretty (y, depth)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
   let
diff -r 366d5726de09 -r 24b8244d672b src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -9,12 +9,12 @@
     (case Future.peek x of
       NONE => str "<future>"
     | SOME (Exn.Exn _) => str "<failed>"
-    | SOME (Exn.Result y) => print (y, depth)));
+    | SOME (Exn.Res y) => print (y, depth)));
 
 PolyML.install_pp
   (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
     (case Lazy.peek x of
       NONE => str "<lazy>"
     | SOME (Exn.Exn _) => str "<failed>"
-    | SOME (Exn.Result y) => print (y, depth)));
+    | SOME (Exn.Res y) => print (y, depth)));
 
diff -r 366d5726de09 -r 24b8244d672b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -252,8 +252,8 @@
             val path = Path.explode thy_name;
             val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
           in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
-      | NONE => Exn.Result raw_tr) of
-    Exn.Result tr =>
+      | NONE => Exn.Res raw_tr) of
+    Exn.Res tr =>
       let
         val is_init = is_some (Toplevel.init_of tr);
         val is_proof = Keyword.is_proof (Toplevel.name_of tr);
diff -r 366d5726de09 -r 24b8244d672b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -197,7 +197,7 @@
 (* decode_term -- transform parse tree into raw term *)
 
 fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
-  | decode_term ctxt (reports0, Exn.Result tm) =
+  | decode_term ctxt (reports0, Exn.Res tm) =
       let
         fun get_const a =
           ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
@@ -259,7 +259,7 @@
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
-fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
+fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
 
 fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
@@ -361,7 +361,7 @@
             else [];
 
           (*brute-force disambiguation via type-inference*)
-          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
+          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
             handle exn as ERROR _ => Exn.Exn exn;
 
           val results' =
diff -r 366d5726de09 -r 24b8244d672b src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -48,7 +48,7 @@
     val result =
       (case tag of
         "0" => Exn.Exn Null
-      | "1" => Exn.Result res
+      | "1" => Exn.Res res
       | "2" => Exn.Exn (ERROR res)
       | "3" => Exn.Exn (Fail res)
       | _ => raise Fail "Bad tag");
diff -r 366d5726de09 -r 24b8244d672b src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/library.scala	Mon Jul 11 23:20:40 2011 +0200
@@ -20,14 +20,19 @@
 {
   /* user errors */
 
+  private val runtime_exception = Class.forName("java.lang.RuntimeException")
+
   object ERROR
   {
     def apply(message: String): Throwable = new RuntimeException(message)
     def unapply(exn: Throwable): Option[String] =
       exn match {
         case e: RuntimeException =>
-          val msg = e.getMessage
-          Some(if (msg == null) "Error" else msg)
+          if (e.getClass != runtime_exception) Some(e.toString)
+          else {
+            val msg = e.getMessage
+            Some(if (msg == null) "Error" else msg)
+          }
         case _ => None
       }
   }
diff -r 366d5726de09 -r 24b8244d672b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -217,7 +217,7 @@
             else
               let val seen' = Inttab.update (i, ()) seen in
                 (case Future.peek body of
-                  SOME (Exn.Result body') => status body' (st, seen')
+                  SOME (Exn.Res body') => status body' (st, seen')
                 | SOME (Exn.Exn _) =>
                     let val (oracle, unfinished, _) = st
                     in ((oracle, unfinished, true), seen') end
diff -r 366d5726de09 -r 24b8244d672b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/thm.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -528,7 +528,7 @@
   let
     val ps = map (Future.peek o snd) promises;
     val bodies = body ::
-      map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+      map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
     val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   in
    {oracle = oracle,
diff -r 366d5726de09 -r 24b8244d672b src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Jul 11 23:20:40 2011 +0200
@@ -214,37 +214,33 @@
             r2 <- r1.try_restrict(chunk_range)
           } yield r2
 
+        val padded_markup =
+          if (markup.isEmpty)
+            Iterator(Text.Info(chunk_range, None))
+          else
+            Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
+            markup.iterator ++
+            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
+
         var x1 = x + w
         gfx.setFont(chunk_font)
-        if (markup.isEmpty) {
-          gfx.setColor(chunk_color)
-          gfx.drawString(chunk.str, x1, y)
-        }
-        else {
-          for {
-            Text.Info(range, info) <-
-              Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
-              markup.iterator ++
-              Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
-            if !range.is_singularity
-          } {
-            val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
-            gfx.setColor(info.getOrElse(chunk_color))
+        for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
+          val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+          gfx.setColor(info.getOrElse(chunk_color))
 
-            range.try_restrict(caret_range) match {
-              case Some(r) if !r.is_singularity =>
-                val astr = new AttributedString(str)
-                val i = r.start - range.start
-                val j = r.stop - range.start
-                astr.addAttribute(TextAttribute.FONT, chunk_font)
-                astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
-                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
-                gfx.drawString(astr.getIterator, x1, y)
-              case _ =>
-                gfx.drawString(str, x1, y)
-            }
-            x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+          range.try_restrict(caret_range) match {
+            case Some(r) if !r.is_singularity =>
+              val astr = new AttributedString(str)
+              val i = r.start - range.start
+              val j = r.stop - range.start
+              astr.addAttribute(TextAttribute.FONT, chunk_font)
+              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
+              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
+              gfx.drawString(astr.getIterator, x1, y)
+            case _ =>
+              gfx.drawString(str, x1, y)
           }
+          x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
         }
       }
       w += chunk.width
diff -r 366d5726de09 -r 24b8244d672b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 11 23:20:40 2011 +0200
@@ -237,9 +237,9 @@
     if Config.get ctxt quiet then
       try tester v
     else
-      let
+      let (* FIXME !?!? *)
         val tester = Exn.interruptible_capture tester v
-      in case Exn.get_result tester of
+      in case Exn.get_res tester of
           NONE => SOME (Exn.release tester)
         | SOME tester => SOME tester
       end