# 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 ""); 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