# HG changeset patch
# User wenzelm
# Date 1293025443 -3600
# Node ID 6476ab765777f63abf88557c36d8620b4dad477c
# Parent  c4488b7cbe3becf435d181b01cf59874bf358f00# Parent  514bb82514dffb4d662f36cf8a0f90b5d9ee7bb5
merged

diff -r c4488b7cbe3b -r 6476ab765777 NEWS
--- a/NEWS	Wed Dec 22 09:02:43 2010 +0100
+++ b/NEWS	Wed Dec 22 14:44:03 2010 +0100
@@ -54,11 +54,15 @@
   show_consts                   show_consts
   show_abbrevs                  show_abbrevs
 
+  Syntax.ast_trace              syntax_ast_trace
+  Syntax.ast_stat               syntax_ast_stat
   Syntax.ambiguity_level        syntax_ambiguity_level
 
   Goal_Display.goals_limit      goals_limit
   Goal_Display.show_main_goal   show_main_goal
 
+  Method.rule_trace             rule_trace
+
   Thy_Output.display            thy_output_display
   Thy_Output.quotes             thy_output_quotes
   Thy_Output.indent             thy_output_indent
diff -r c4488b7cbe3b -r 6476ab765777 lib/Tools/java
--- a/lib/Tools/java	Wed Dec 22 09:02:43 2010 +0100
+++ b/lib/Tools/java	Wed Dec 22 14:44:03 2010 +0100
@@ -5,4 +5,12 @@
 # DESCRIPTION: invoke Java within the Isabelle environment
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "${THIS_JAVA:-$ISABELLE_JAVA}" "$@"
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+if "$JAVA_EXE" -server >/dev/null 2>/dev/null
+then
+  exec "$JAVA_EXE" -server "$@"
+else
+  exec "$JAVA_EXE" "$@"
+fi
+
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -398,13 +398,16 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_brackets_raw #>
+ (register_config Syntax.ast_trace_raw #>
+  register_config Syntax.ast_stat_raw #>
+  register_config Syntax.show_brackets_raw #>
   register_config Syntax.show_sorts_raw #>
   register_config Syntax.show_types_raw #>
   register_config Syntax.show_structs_raw #>
   register_config Syntax.show_question_marks_raw #>
   register_config Syntax.ambiguity_level_raw #>
   register_config Syntax.eta_contract_raw #>
+  register_config ML_Context.trace_raw #>
   register_config ProofContext.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
   register_config Goal_Display.show_main_goal_raw #>
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/Isar/method.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
   val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-  val trace_rules: bool Unsynchronized.ref
+  val rule_trace: bool Config.T
 end;
 
 signature METHOD =
@@ -218,10 +218,10 @@
 
 (* rule etc. -- single-step refinements *)
 
-val trace_rules = Unsynchronized.ref false;
+val (rule_trace, rule_trace_setup) = Attrib.config_bool "rule_trace" (fn _ => false);
 
 fun trace ctxt rules =
-  if ! trace_rules andalso not (null rules) then
+  if Config.get ctxt rule_trace andalso not (null rules) then
     Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
     |> Pretty.string_of |> tracing
   else ();
@@ -438,7 +438,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
+ (rule_trace_setup #>
+  setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
   setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
   setup (Binding.name "-") (Scan.succeed (K insert_facts))
     "do nothing (insert current facts only)" #>
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -48,7 +48,7 @@
     let
       val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
-      val body = "Isabelle." ^ a;
+      val body = " Isabelle." ^ a ^ " ";
     in (K (env, body), background') end));
 
 val value = declaration "val";
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -25,7 +25,8 @@
   val ml_store_thm: string * thm -> unit
   type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
   val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
-  val trace: bool Unsynchronized.ref
+  val trace_raw: Config.raw
+  val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -172,7 +173,8 @@
         in (ml, SOME (Context.Proof ctxt')) end;
   in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
 
-val trace = Unsynchronized.ref false;
+val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
+val trace = Config.bool trace_raw;
 
 fun eval verbose pos ants =
   let
@@ -181,8 +183,12 @@
       eval_antiquotes (ants, pos) (Context.thread_data ())
       ||> Option.map (Context.mapping I (Context_Position.set_visible false));
     val _ =
-      if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
-      else ();
+      (case env_ctxt of
+        SOME context =>
+          if Config.get (Context.proof_of context) trace then
+            tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
+          else ()
+      | NONE => ());
 
     (*prepare static ML environment*)
     val _ = Context.setmp_thread_data env_ctxt
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -39,7 +39,7 @@
       val i = serial ();
       val (a, background') = background
         |> ML_Antiquote.variant kind ||> put_thms (i, ths);
-      val ml = (thm_bind kind a i, "Isabelle." ^ a);
+      val ml = (thm_bind kind a i, " Isabelle." ^ a ^ " ");
     in (K ml, background') end));
 
 val _ = thm_antiq "thm" (Attrib.thm >> single);
@@ -69,7 +69,8 @@
         val (a, background') = background
           |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
         val ml =
-          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
+          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i,
+            " Isabelle." ^ a ^ " ");
       in (K ml, background') end));
 
 end;
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -153,9 +153,6 @@
   nat_pref Raw_Simplifier.simp_trace_depth_limit_default
     "trace-simplifier-depth"
     "Trace simplifier depth limit.",
-  bool_pref trace_rules
-    "trace-rules"
-    "Trace application of the standard rules",
   bool_pref Pattern.trace_unify_fail
     "trace-unification"
     "Output error diagnostics during unification",
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/Syntax/ast.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -24,8 +24,10 @@
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
-  val trace_ast: bool Unsynchronized.ref
-  val stat_ast: bool Unsynchronized.ref
+  val ast_trace_raw: Config.raw
+  val ast_trace: bool Config.T
+  val ast_stat_raw: Config.raw
+  val ast_stat: bool Config.T
 end;
 
 signature AST =
@@ -33,8 +35,7 @@
   include AST1
   val head_of_rule: ast * ast -> string
   val rule_error: ast * ast -> string option
-  val normalize: bool -> bool -> (string -> (ast * ast) list) -> ast -> ast
-  val normalize_ast: (string -> (ast * ast) list) -> ast -> ast
+  val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
 end;
 
 structure Ast : AST =
@@ -168,10 +169,18 @@
 
 (* normalize *)
 
-(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
+val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
+val ast_trace = Config.bool ast_trace_raw;
+
+val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
+val ast_stat = Config.bool ast_stat_raw;
 
-fun normalize trace stat get_rules pre_ast =
+(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
+fun normalize ctxt get_rules pre_ast =
   let
+    val trace = Config.get ctxt ast_trace;
+    val stat = Config.get ctxt ast_stat;
+
     val passes = Unsynchronized.ref 0;
     val failed_matches = Unsynchronized.ref 0;
     val changes = Unsynchronized.ref 0;
@@ -241,13 +250,4 @@
       else ();
   in post_ast end;
 
-
-(* normalize_ast *)
-
-val trace_ast = Unsynchronized.ref false;
-val stat_ast = Unsynchronized.ref false;
-
-fun normalize_ast get_rules ast =
-  normalize (! trace_ast) (! stat_ast) get_rules ast;
-
 end;
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -17,7 +17,7 @@
     Tip of Lexicon.token
   val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
   val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
-  val branching_level: int Unsynchronized.ref
+  val branching_level: int Config.T
 end;
 
 structure Parser: PARSER =
@@ -715,7 +715,8 @@
       else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
 
 
-val branching_level = Unsynchronized.ref 600;   (*trigger value for warnings*)
+(*trigger value for warnings*)
+val branching_level = Config.int (Config.declare "syntax_branching_level" (fn _ => Config.Int 600));
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
@@ -771,7 +772,7 @@
 
                 val dummy =
                   if not (! warned) andalso
-                     length (new_states @ States) > ! branching_level then
+                     length (new_states @ States) > Config.get ctxt branching_level then
                     (Context_Position.if_visible ctxt warning
                       "Currently parsed expression could be extremely ambiguous";
                      warned := true)
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -736,7 +736,7 @@
     val asts = read_asts ctxt syn false root inp;
   in
     Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
-      (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
+      (map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) asts)
   end;
 
 
@@ -871,7 +871,7 @@
   in
     Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (print_mode_value ()))
-      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
+      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
   end;
 
 in
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/System/gui_setup.scala	Wed Dec 22 14:44:03 2010 +0100
@@ -39,7 +39,7 @@
     // values
     if (Platform.is_windows)
       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
-    text.append("JVM name: " + System.getProperty("java.vm.name") + "\n")
+    text.append("JVM name: " + Platform.jvm_name + "\n")
     text.append("JVM platform: " + Platform.jvm_platform + "\n")
     try {
       val isabelle_system = new Isabelle_System
diff -r c4488b7cbe3b -r 6476ab765777 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Pure/System/platform.scala	Wed Dec 22 14:44:03 2010 +0100
@@ -53,6 +53,12 @@
   }
 
 
+  /* JVM name */
+
+  val jvm_name: String = java.lang.System.getProperty("java.vm.name")
+  val is_hotspot: Boolean = jvm_name.startsWith("Java HotSpot")
+
+
   /* Swing look-and-feel */
 
   private def find_laf(name: String): Option[String] =
diff -r c4488b7cbe3b -r 6476ab765777 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Dec 22 14:44:03 2010 +0100
@@ -228,16 +228,13 @@
 
 fun register_const const = register_code [] [const];
 
-fun print_const const all_struct_name consts_map =
-  (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
-
 fun print_code is_first const ctxt =
   let
     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
     val (ml_code, consts_map) = Lazy.force acc_code;
     val ml_code = if is_first then ml_code else "";
-    val all_struct_name = "Isabelle";
-  in (ml_code, print_const const all_struct_name consts_map) end;
+    val body = " Isabelle." ^ the (AList.lookup (op =) consts_map const) ^ " ";
+  in (ml_code, body) end;
 
 in
 
diff -r c4488b7cbe3b -r 6476ab765777 src/Tools/jEdit/dist-template/lib/Tools/jedit
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Dec 22 14:44:03 2010 +0100
@@ -78,9 +78,6 @@
 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
 [ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
 
-"$ISABELLE_TOOL" java -server >/dev/null 2>/dev/null && \
-  JAVA_ARGS["${#JAVA_ARGS[@]}"]="-server"
-
 declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
 
 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
diff -r c4488b7cbe3b -r 6476ab765777 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 22 09:02:43 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 22 14:44:03 2010 +0100
@@ -143,6 +143,18 @@
   }
 
 
+  /* check JVM */
+
+  def check_jvm()
+  {
+    if (!Platform.is_hotspot) {
+      Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
+        "This is " + Platform.jvm_name,
+        "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
+    }
+  }
+
+
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
@@ -332,8 +344,9 @@
   override def handleMessage(message: EBMessage)
   {
     message match {
-      case msg: EditorStarted
-      if Isabelle.Boolean_Property("auto-start") => Isabelle.start_session()
+      case msg: EditorStarted =>
+      Isabelle.check_jvm()
+      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
 
       case msg: BufferUpdate
       if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>