# HG changeset patch
# User wenzelm
# Date 1305212335 -7200
# Node ID ab07cb4513903df9949656db96127215a7ae39c6
# Parent  e588d3e8ad911e36caaa70739cb94203cb48732e# Parent  dfeec3aaae9d51ade184d2804753d1c4db354ec7
merged

diff -r e588d3e8ad91 -r ab07cb451390 lib/scripts/isabelle-platform
--- a/lib/scripts/isabelle-platform	Thu May 12 16:48:23 2011 +0200
+++ b/lib/scripts/isabelle-platform	Thu May 12 16:58:55 2011 +0200
@@ -57,10 +57,10 @@
         ;;
     esac
     ;;
-  FreeBSD|NetBSD)
+  *BSD)
     case $(uname -m) in
       i?86 | x86_64)
-        ISABELLE_PLATFORM=x86-bsd
+        ISABELLE_PLATFORM=x86-linux
         ;;
     esac
     ;;
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/General/linear_set.scala	Thu May 12 16:58:55 2011 +0200
@@ -14,7 +14,7 @@
 
 object Linear_Set extends ImmutableSetFactory[Linear_Set]
 {
-  private case class Rep[A](
+  protected case class Rep[A](
     val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
 
   private def empty_rep[A] = Rep[A](None, None, Map(), Map())
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/General/scan.scala	Thu May 12 16:58:55 2011 +0200
@@ -22,7 +22,7 @@
 
   object Lexicon
   {
-    private case class Tree(val branches: Map[Char, (String, Tree)])
+    protected case class Tree(val branches: Map[Char, (String, Tree)])
     private val empty_tree = Tree(Map())
 
     val empty: Lexicon = new Lexicon
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/General/yxml.scala	Thu May 12 16:58:55 2011 +0200
@@ -121,7 +121,7 @@
         }
       }
     }
-    stack match {
+    (stack: @unchecked) match {
       case List((Markup.Empty, body)) => body.toList
       case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/Isar/proof.ML	Thu May 12 16:58:55 2011 +0200
@@ -31,7 +31,6 @@
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
-  val verbose: bool Unsynchronized.ref
   val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
@@ -324,8 +323,6 @@
 
 (** pretty_state **)
 
-val verbose = Proof_Context.verbose;
-
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
       [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
@@ -333,6 +330,7 @@
 fun pretty_state nr state =
   let
     val {context = ctxt, facts, mode, goal = _} = current state;
+    val verbose = Config.get ctxt Proof_Context.verbose;
 
     fun levels_up 0 = ""
       | levels_up 1 = "1 level up"
@@ -357,15 +355,15 @@
       | prt_goal NONE = [];
 
     val prt_ctxt =
-      if ! verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
+      if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
       else [];
   in
     [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
-      (if ! verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
+      (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
       Pretty.str ""] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
-    (if ! verbose orelse mode = Forward then
+    (if verbose orelse mode = Forward then
        pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
      else if mode = Chain then pretty_facts "picking " ctxt facts
      else prt_goal (try find_goal state))
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 12 16:58:55 2011 +0200
@@ -151,8 +151,8 @@
   val print_binds: Proof.context -> unit
   val print_lthms: Proof.context -> unit
   val print_cases: Proof.context -> unit
-  val debug: bool Unsynchronized.ref
-  val verbose: bool Unsynchronized.ref
+  val debug: bool Config.T
+  val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
 end;
@@ -1235,11 +1235,11 @@
 
 (* core context *)
 
-val debug = Unsynchronized.ref false;
-val verbose = Unsynchronized.ref false;
+val debug = Config.bool (Config.declare "Proof_Context.debug" (K (Config.Bool false)));
+val verbose = Config.bool (Config.declare "Proof_Context.verbose" (K (Config.Bool false)));
 
 fun pretty_ctxt ctxt =
-  if not (! debug) then []
+  if not (Config.get ctxt debug) then []
   else
     let
       val prt_term = Syntax.pretty_term ctxt;
@@ -1275,8 +1275,8 @@
 
 fun pretty_context ctxt =
   let
-    val is_verbose = ! verbose;
-    fun verb f x = if is_verbose then f (x ()) else [];
+    val verbose = Config.get ctxt verbose;
+    fun verb f x = if verbose then f (x ()) else [];
 
     val prt_term = Syntax.pretty_term ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu May 12 16:58:55 2011 +0200
@@ -27,7 +27,7 @@
 (* toplevel pretty printing *)
 
 fun pp_context ctxt =
- (if ! Proof_Context.debug then
+ (if Config.get ctxt Proof_Context.debug then
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");
 
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu May 12 16:48:23 2011 +0200
+++ b/src/Pure/build-jars	Thu May 12 16:58:55 2011 +0200
@@ -63,6 +63,7 @@
   Thy/thy_header.scala
   Thy/thy_syntax.scala
   library.scala
+  package.scala
 )
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
diff -r e588d3e8ad91 -r ab07cb451390 src/Pure/package.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/package.scala	Thu May 12 16:58:55 2011 +0200
@@ -0,0 +1,11 @@
+/*  Title:      Pure/package.scala
+    Author:     Makarius
+
+Toplevel isabelle package.
+*/
+
+package object isabelle
+{
+  def error(message: String): Nothing = throw new RuntimeException(message)
+}
+
diff -r e588d3e8ad91 -r ab07cb451390 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Thu May 12 16:48:23 2011 +0200
+++ b/src/Tools/jEdit/README_BUILD	Thu May 12 16:58:55 2011 +0200
@@ -2,7 +2,7 @@
 Requirements to build from sources
 ==================================
 
-* Proper Java JRE/JDK from Sun, e.g. 1.6.0_21
+* Proper Java JRE/JDK from Sun, e.g. 1.6.0_24
   http://java.sun.com/javase/downloads/index.jsp
 
 * Netbeans 6.9
@@ -31,7 +31,7 @@
 * Isabelle/Pure Scala components
   Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar
 
-* Scala Compiler 2.8.1.final
+* Scala Compiler 2.8.1.final or 2.9.0.final
   http://www.scala-lang.org
   Netbeans Library "Scala-compiler" = $SCALA_HOME/lib/scala-compiler.jar