--- 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
--- 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
+
--- 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 #>
--- 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)" #>
--- 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";
--- 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
--- 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;
--- 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",
--- 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;
--- 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)
--- 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
--- 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
--- 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] =
--- 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
--- 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)"
--- 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 =>