--- 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
;;
--- 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())
--- 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
--- 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)
}
--- 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))
--- 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;
--- 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>");
--- 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"
--- /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)
+}
+
--- 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