# HG changeset patch
# User wenzelm
# Date 1473190608 -7200
# Node ID 5f8643e8ced5a968819eb58113eb32029e222c0c
# Parent  761f81af24581459e43b20e769e24ce7cde17d25# Parent  3a75593e9b6d1d0c41d1d38d8c02e5a585b6357b
merged

diff -r 761f81af2458 -r 5f8643e8ced5 NEWS
--- a/NEWS	Tue Sep 06 15:23:01 2016 +0200
+++ b/NEWS	Tue Sep 06 21:36:48 2016 +0200
@@ -334,8 +334,12 @@
     INCOMPATIBILITY.
   - The "size" plugin has been made compatible again with locales.
 
-* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
-linorder_cases instead.
+* Some old / obsolete theorems have been renamed / removed, potential
+INCOMPATIBILITY.
+
+  nat_less_cases  --  removed, use linorder_cases instead
+  inv_image_comp  --  removed, use image_inv_f_f instead
+  image_surj_f_inv_f  ~>  image_f_inv_f
 
 * Some theorems about groups and orders have been generalised from
   groups to semi-groups that are also monoids:
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -2386,7 +2386,7 @@
   have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P
     apply safe
     apply (rule_tac x="inv h ` x" in image_eqI)
-    apply (auto simp: \<open>bij h\<close> bij_is_surj image_surj_f_inv_f)
+    apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f)
     done
   have "inj h" using bij_is_inj assms by blast
   then have injim: "inj_on (op ` h) A" for A
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -98,7 +98,7 @@
 
 code_reserved Eval Code_Evaluation
 
-ML_file "~~/src/HOL/Tools/value.ML"
+ML_file "~~/src/HOL/Tools/value_command.ML"
 
 
 subsection \<open>\<open>term_of\<close> instances\<close>
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -80,7 +80,7 @@
   by (rule chainI) simp
 
 lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
-  by (rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+  by (rule antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
 
 
 subsection \<open>Transfinite iteration of a function\<close>
@@ -282,26 +282,6 @@
 context ccpo
 begin
 
-lemma admissible_disj_lemma:
-  assumes A: "chain (op \<le>)A"
-  assumes P: "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y"
-  shows "Sup A = Sup {x \<in> A. P x}"
-proof (rule antisym)
-  have *: "chain (op \<le>) {x \<in> A. P x}"
-    by (rule chain_compr [OF A])
-  show "Sup A \<le> Sup {x \<in> A. P x}"
-    apply (rule ccpo_Sup_least [OF A])
-    apply (drule P [rule_format], clarify)
-    apply (erule order_trans)
-    apply (simp add: ccpo_Sup_upper [OF *])
-    done
-  show "Sup {x \<in> A. P x} \<le> Sup A"
-    apply (rule ccpo_Sup_least [OF *])
-    apply clarify
-    apply (simp add: ccpo_Sup_upper [OF A])
-    done
-qed
-
 lemma admissible_disj:
   fixes P Q :: "'a \<Rightarrow> bool"
   assumes P: "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x)"
@@ -309,23 +289,73 @@
   shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
 proof (rule ccpo.admissibleI)
   fix A :: "'a set"
-  assume A: "chain (op \<le>) A"
-  assume "A \<noteq> {}" and "\<forall>x\<in>A. P x \<or> Q x"
-  then have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
-    using chainD[OF A] by blast  (* slow *)
-  then have "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
-    using admissible_disj_lemma [OF A] by blast
+  assume chain: "chain (op \<le>) A"
+  assume A: "A \<noteq> {}" and P_Q: "\<forall>x\<in>A. P x \<or> Q x"
+  have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
+    (is "?P \<or> ?Q" is "?P1 \<and> ?P2 \<or> _")
+  proof (rule disjCI)
+    assume "\<not> ?Q"
+    then consider "\<forall>x\<in>A. \<not> Q x" | a where "a \<in> A" "\<forall>y\<in>A. a \<le> y \<longrightarrow> \<not> Q y"
+      by blast
+    then show ?P
+    proof cases
+      case 1
+      with P_Q have "\<forall>x\<in>A. P x" by blast
+      with A show ?P by blast
+    next
+      case 2
+      note a = \<open>a \<in> A\<close>
+      show ?P
+      proof
+        from P_Q 2 have *: "\<forall>y\<in>A. a \<le> y \<longrightarrow> P y" by blast
+        with a have "P a" by blast
+        with a show ?P1 by blast
+        show ?P2
+        proof
+          fix x
+          assume x: "x \<in> A"
+          with chain a show "\<exists>y\<in>A. x \<le> y \<and> P y"
+          proof (rule chainE)
+            assume le: "a \<le> x"
+            with * a x have "P x" by blast
+            with x le show ?thesis by blast
+          next
+            assume "a \<ge> x"
+            with a \<open>P a\<close> show ?thesis by blast
+          qed
+        qed
+      qed
+    qed
+  qed
+  moreover
+  have "Sup A = Sup {x \<in> A. P x}" if "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y" for P
+  proof (rule antisym)
+    have chain_P: "chain (op \<le>) {x \<in> A. P x}"
+      by (rule chain_compr [OF chain])
+    show "Sup A \<le> Sup {x \<in> A. P x}"
+      apply (rule ccpo_Sup_least [OF chain])
+      apply (drule that [rule_format])
+      apply clarify
+      apply (erule order_trans)
+      apply (simp add: ccpo_Sup_upper [OF chain_P])
+      done
+    show "Sup {x \<in> A. P x} \<le> Sup A"
+      apply (rule ccpo_Sup_least [OF chain_P])
+      apply clarify
+      apply (simp add: ccpo_Sup_upper [OF chain])
+      done
+  qed
+  ultimately
+  consider "\<exists>x. x \<in> A \<and> P x" "Sup A = Sup {x \<in> A. P x}"
+    | "\<exists>x. x \<in> A \<and> Q x" "Sup A = Sup {x \<in> A. Q x}"
+    by blast
   then show "P (Sup A) \<or> Q (Sup A)"
-    apply (rule disjE)
+    apply cases
      apply simp_all
      apply (rule disjI1)
-     apply (rule ccpo.admissibleD [OF P chain_compr [OF A]])
-      apply simp
-     apply simp
+     apply (rule ccpo.admissibleD [OF P chain_compr [OF chain]]; simp)
     apply (rule disjI2)
-    apply (rule ccpo.admissibleD [OF Q chain_compr [OF A]])
-     apply simp
-    apply simp
+    apply (rule ccpo.admissibleD [OF Q chain_compr [OF chain]]; simp)
     done
 qed
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -244,15 +244,12 @@
 lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
   by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
 
-lemma image_surj_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
+lemma image_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
   by (simp add: surj_f_inv_f image_comp comp_def)
 
 lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
   by simp
 
-lemma inv_image_comp: "inj f \<Longrightarrow> inv f ` (f ` X) = X"
-  by (fact image_inv_f_f)
-
 lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
   apply auto
    apply (force simp add: bij_is_inj)
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Library/code_test.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -579,7 +579,7 @@
    (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    (scalaN, (evaluate_in_scala, Code_Scala.target))]
-  #> fold (fn target => Value.add_evaluator (target, eval_term target))
+  #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
     [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
 
 end
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -626,7 +626,7 @@
             Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
           val trivial =
             if AList.lookup (op =) args check_trivialK |> the_default trivial_default
-                            |> Markup.parse_bool then
+                            |> Value.parse_bool then
               Try0.try0 (SOME try_timeout) ([], [], [], []) pre
               handle Timeout.TIMEOUT _ => false
             else false
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -7,7 +7,7 @@
 
 fun get args name default_value =
   case AList.lookup (op =) args name of
-    SOME value => Markup.parse_real value
+    SOME value => Value.parse_real value
   | NONE => default_value
 
 fun extract_relevance_fudge args
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Tue Sep 06 15:23:01 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-(*  Title:      HOL/Tools/value.ML
-    Author:     Florian Haftmann, TU Muenchen
-
-Generic value command for arbitrary evaluators, with default using nbe or SML.
-*)
-
-signature VALUE =
-sig
-  val value: Proof.context -> term -> term
-  val value_select: string -> Proof.context -> term -> term
-  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
-  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
-end;
-
-structure Value : VALUE =
-struct
-
-fun default_value ctxt t =
-  if null (Term.add_frees t [])
-  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
-    SOME t' => t'
-  | NONE => Nbe.dynamic_value ctxt t
-  else Nbe.dynamic_value ctxt t;
-
-structure Evaluator = Theory_Data
-(
-  type T = (string * (Proof.context -> term -> term)) list;
-  val empty = [("default", default_value)];
-  val extend = I;
-  fun merge data : T = AList.merge (op =) (K true) data;
-)
-
-val add_evaluator = Evaluator.map o AList.update (op =);
-
-fun value_select name ctxt =
-  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
-   of NONE => error ("No such evaluator: " ^ name)
-    | SOME f => f ctxt;
-
-fun value ctxt =
-  let
-    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
-  in
-    if null evaluators
-    then error "No evaluators"
-    else (snd o snd o split_last) evaluators ctxt
-  end;
-
-fun value_maybe_select some_name =
-  case some_name
-    of NONE => value
-     | SOME name => value_select name;
-  
-fun value_cmd some_name modes raw_t state =
-  let
-    val ctxt = Toplevel.context_of state;
-    val t = Syntax.read_term ctxt raw_t;
-    val t' = value_maybe_select some_name ctxt t;
-    val ty' = Term.type_of t';
-    val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = Print_Mode.with_modes modes (fn () =>
-      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
-
-val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
-
-val opt_evaluator =
-  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
-  
-val _ =
-  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
-    (opt_evaluator -- opt_modes -- Parse.term
-      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
-
-val _ = Theory.setup
-  (Thy_Output.antiquotation @{binding value}
-    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
-    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
-      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
-        [style (value_maybe_select some_name context t)]))
-  #> add_evaluator ("simp", Code_Simp.dynamic_value)
-  #> add_evaluator ("nbe", Nbe.dynamic_value)
-  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
-
-end;
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/Tools/value_command.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/value_command.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -0,0 +1,87 @@
+(*  Title:      HOL/Tools/value_command.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Generic value command for arbitrary evaluators, with default using nbe or SML.
+*)
+
+signature VALUE_COMMAND =
+sig
+  val value: Proof.context -> term -> term
+  val value_select: string -> Proof.context -> term -> term
+  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
+  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
+end;
+
+structure Value_Command : VALUE_COMMAND =
+struct
+
+fun default_value ctxt t =
+  if null (Term.add_frees t [])
+  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
+    SOME t' => t'
+  | NONE => Nbe.dynamic_value ctxt t
+  else Nbe.dynamic_value ctxt t;
+
+structure Evaluator = Theory_Data
+(
+  type T = (string * (Proof.context -> term -> term)) list;
+  val empty = [("default", default_value)];
+  val extend = I;
+  fun merge data : T = AList.merge (op =) (K true) data;
+)
+
+val add_evaluator = Evaluator.map o AList.update (op =);
+
+fun value_select name ctxt =
+  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
+   of NONE => error ("No such evaluator: " ^ name)
+    | SOME f => f ctxt;
+
+fun value ctxt =
+  let
+    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
+  in
+    if null evaluators
+    then error "No evaluators"
+    else (snd o snd o split_last) evaluators ctxt
+  end;
+
+fun value_maybe_select some_name =
+  case some_name
+    of NONE => value
+     | SOME name => value_select name;
+  
+fun value_cmd some_name modes raw_t state =
+  let
+    val ctxt = Toplevel.context_of state;
+    val t = Syntax.read_term ctxt raw_t;
+    val t' = value_maybe_select some_name ctxt t;
+    val ty' = Term.type_of t';
+    val ctxt' = Variable.auto_fixes t' ctxt;
+    val p = Print_Mode.with_modes modes (fn () =>
+      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+  in Pretty.writeln p end;
+
+val opt_modes =
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
+
+val opt_evaluator =
+  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
+  
+val _ =
+  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
+    (opt_evaluator -- opt_modes -- Parse.term
+      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding value}
+    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
+    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
+      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
+        [style (value_maybe_select some_name context t)]))
+  #> add_evaluator ("simp", Code_Simp.dynamic_value)
+  #> add_evaluator ("nbe", Nbe.dynamic_value)
+  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
+
+end;
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/UNITY/Rename.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -10,7 +10,7 @@
 definition rename :: "['a => 'b, 'a program] => 'b program" where
     "rename h == extend (%(x,u::unit). h x)"
 
-declare image_inv_f_f [simp] image_surj_f_inv_f [simp]
+declare image_inv_f_f [simp] image_f_inv_f [simp]
 
 declare Extend.intro [simp,intro]
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/HOL/ex/Set_Theory.thy
--- a/src/HOL/ex/Set_Theory.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/HOL/ex/Set_Theory.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -108,7 +108,7 @@
     apply (rule_tac [2] inj_on_inv_into)
     apply (erule subset_inj_on [OF _ subset_UNIV])
    apply blast
-  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
+  apply (erule ssubst, subst double_complement, erule image_inv_f_f [symmetric])
   done
 
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -171,15 +171,15 @@
       val active = count_workers Working;
       val waiting = count_workers Waiting;
       val stats =
-       [("now", Markup.print_real (Time.toReal (Time.now ()))),
-        ("tasks_ready", Markup.print_int ready),
-        ("tasks_pending", Markup.print_int pending),
-        ("tasks_running", Markup.print_int running),
-        ("tasks_passive", Markup.print_int passive),
-        ("tasks_urgent", Markup.print_int urgent),
-        ("workers_total", Markup.print_int total),
-        ("workers_active", Markup.print_int active),
-        ("workers_waiting", Markup.print_int waiting)] @
+       [("now", Value.print_real (Time.toReal (Time.now ()))),
+        ("tasks_ready", Value.print_int ready),
+        ("tasks_pending", Value.print_int pending),
+        ("tasks_running", Value.print_int running),
+        ("tasks_passive", Value.print_int passive),
+        ("tasks_urgent", Value.print_int urgent),
+        ("workers_total", Value.print_int total),
+        ("workers_active", Value.print_int active),
+        ("workers_waiting", Value.print_int waiting)] @
         ML_Statistics.get ();
     in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
   else ();
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -31,7 +31,7 @@
   in Exn_Properties.update (update_serial @ update_props) exn end;
 
 fun the_serial exn =
-  Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
+  Value.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
 
 val exn_ord = rev_order o int_ord o apply2 the_serial;
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Concurrent/standard_thread.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -31,7 +31,7 @@
 
   lazy val pool: ThreadPoolExecutor =
     {
-      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+      val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
       val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
       val executor =
         new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -152,8 +152,8 @@
       (case timing of NONE => timing_start | SOME var => Synchronized.value var);
     fun micros time = string_of_int (Time.toNanoseconds time div 1000);
   in
-    [("now", Markup.print_real (Time.toReal (Time.now ()))),
-     ("task_name", name), ("task_id", Markup.print_int id),
+    [("now", Value.print_real (Time.toReal (Time.now ()))),
+     ("task_name", name), ("task_id", Value.print_int id),
      ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
     Position.properties_of pos
   end;
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/General/completion.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -402,23 +402,26 @@
   }
 
   def add_abbrevs(abbrevs: List[(String, String)]): Completion =
-    if (abbrevs.isEmpty) this
-    else {
-      val words =
-        for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
-          yield (abbr, text)
-      val abbrs =
-        for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
-          yield (abbr.reverse, (abbr, text))
-      val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
+    (this /: abbrevs)(_.add_abbrev(_))
+
+  private def add_abbrev(abbrev: (String, String)): Completion =
+  {
+    val (abbr, text) = abbrev
+    val rev_abbr = abbr.reverse
+    val is_word = Completion.Word_Parsers.is_word(abbr)
 
-      new Completion(
-        keywords,
-        words_lex ++ words.map(_._1) -- remove,
-        words_map ++ words -- remove,
-        abbrevs_lex ++ abbrs.map(_._1) -- remove,
-        abbrevs_map ++ abbrs -- remove)
-    }
+    val (words_lex1, words_map1) =
+      if (!is_word) (words_lex, words_map)
+      else if (text != "") (words_lex + abbr, words_map + abbrev)
+      else (words_lex -- List(abbr), words_map - abbr)
+
+    val (abbrevs_lex1, abbrevs_map1) =
+      if (is_word) (abbrevs_lex, abbrevs_map)
+      else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
+      else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
+
+    new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+  }
 
   private def load(): Completion =
     add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/General/position.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -137,7 +137,7 @@
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
 
-fun parse_id pos = Option.map Markup.parse_int (get_id pos);
+fun parse_id pos = Option.map Value.parse_int (get_id pos);
 
 
 (* markup properties *)
@@ -145,7 +145,7 @@
 fun get props name =
   (case Properties.get props name of
     NONE => 0
-  | SOME s => Markup.parse_int s);
+  | SOME s => Value.parse_int s);
 
 fun of_properties props =
   make {line = get props Markup.lineN,
@@ -153,7 +153,7 @@
     end_offset = get props Markup.end_offsetN,
     props = props};
 
-fun value k i = if valid i then [(k, Markup.print_int i)] else [];
+fun value k i = if valid i then [(k, Value.print_int i)] else [];
 
 fun properties_of (Pos ((i, j, k), props)) =
   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
@@ -161,8 +161,8 @@
 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
 
 fun entity_properties_of def serial pos =
-  if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
-  else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
+  if def then (Markup.defN, Value.print_int serial) :: properties_of pos
+  else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
 
 fun default_properties default props =
   if exists (member (op =) Markup.position_properties o #1) props then props
@@ -205,8 +205,8 @@
     val props = properties_of pos;
     val (s1, s2) =
       (case (line_of pos, file_of pos) of
-        (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
-      | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
+        (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
+      | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
       | _ => if is_reported pos then ("", "\<here>") else ("", ""));
   in
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/General/properties.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -10,55 +10,6 @@
 
 object Properties
 {
-  /* plain values */
-
-  object Value
-  {
-    object Boolean
-    {
-      def apply(x: scala.Boolean): java.lang.String = x.toString
-      def unapply(s: java.lang.String): Option[scala.Boolean] =
-        s match {
-          case "true" => Some(true)
-          case "false" => Some(false)
-          case _ => None
-        }
-      def parse(s: java.lang.String): scala.Boolean =
-        unapply(s) getOrElse error("Bad boolean: " + quote(s))
-    }
-
-    object Int
-    {
-      def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
-      def unapply(s: java.lang.String): Option[scala.Int] =
-        try { Some(Integer.parseInt(s)) }
-        catch { case _: NumberFormatException => None }
-      def parse(s: java.lang.String): scala.Int =
-        unapply(s) getOrElse error("Bad integer: " + quote(s))
-    }
-
-    object Long
-    {
-      def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
-      def unapply(s: java.lang.String): Option[scala.Long] =
-        try { Some(java.lang.Long.parseLong(s)) }
-        catch { case _: NumberFormatException => None }
-      def parse(s: java.lang.String): scala.Long =
-        unapply(s) getOrElse error("Bad integer: " + quote(s))
-    }
-
-    object Double
-    {
-      def apply(x: scala.Double): java.lang.String = x.toString
-      def unapply(s: java.lang.String): Option[scala.Double] =
-        try { Some(java.lang.Double.parseDouble(s)) }
-        catch { case _: NumberFormatException => None }
-      def parse(s: java.lang.String): scala.Double =
-        unapply(s) getOrElse error("Bad real: " + quote(s))
-    }
-  }
-
-
   /* named entries */
 
   type Entry = (java.lang.String, java.lang.String)
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/General/sqlite.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -29,6 +29,8 @@
 
     def close { connection.close }
 
+    def rebuild { using(statement("VACUUM"))(_.execute()) }
+
     def transaction[A](body: => A): A =
     {
       val auto_commit = connection.getAutoCommit
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/General/value.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/value.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -0,0 +1,57 @@
+(*  Title:      Pure/General/value.ML
+    Author:     Makarius
+
+Plain values, represented as string.
+*)
+
+signature VALUE =
+sig
+  val parse_bool: string -> bool
+  val print_bool: bool -> string
+  val parse_nat: string -> int
+  val parse_int: string -> int
+  val print_int: int -> string
+  val parse_real: string -> real
+  val print_real: real -> string
+end;
+
+structure Value: VALUE =
+struct
+
+fun parse_bool "true" = true
+  | parse_bool "false" = false
+  | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
+
+val print_bool = Bool.toString;
+
+
+fun parse_nat s =
+  let val i = Int.fromString s in
+    if is_none i orelse the i < 0
+    then raise Fail ("Bad natural number " ^ quote s)
+    else the i
+  end;
+
+fun parse_int s =
+  let val i = Int.fromString s in
+    if is_none i orelse String.isPrefix "~" s
+    then raise Fail ("Bad integer " ^ quote s)
+    else the i
+  end;
+
+val print_int = signed_string_of_int;
+
+
+fun parse_real s =
+  (case Real.fromString s of
+    SOME x => x
+  | NONE => raise Fail ("Bad real " ^ quote s));
+
+fun print_real x =
+  let val s = signed_string_of_real x in
+    (case space_explode "." s of
+      [a, b] => if forall_string (fn c => c = "0") b then a else s
+    | _ => s)
+  end;
+
+end;
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/General/value.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/value.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -0,0 +1,54 @@
+/*  Title:      Pure/General/value.scala
+    Author:     Makarius
+
+Plain values, represented as string.
+*/
+
+package isabelle
+
+
+object Value
+{
+  object Boolean
+  {
+    def apply(x: scala.Boolean): java.lang.String = x.toString
+    def unapply(s: java.lang.String): Option[scala.Boolean] =
+      s match {
+        case "true" => Some(true)
+        case "false" => Some(false)
+        case _ => None
+      }
+    def parse(s: java.lang.String): scala.Boolean =
+      unapply(s) getOrElse error("Bad boolean: " + quote(s))
+  }
+
+  object Int
+  {
+    def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
+    def unapply(s: java.lang.String): Option[scala.Int] =
+      try { Some(Integer.parseInt(s)) }
+      catch { case _: NumberFormatException => None }
+    def parse(s: java.lang.String): scala.Int =
+      unapply(s) getOrElse error("Bad integer: " + quote(s))
+  }
+
+  object Long
+  {
+    def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
+    def unapply(s: java.lang.String): Option[scala.Long] =
+      try { Some(java.lang.Long.parseLong(s)) }
+      catch { case _: NumberFormatException => None }
+    def parse(s: java.lang.String): scala.Long =
+      unapply(s) getOrElse error("Bad integer: " + quote(s))
+  }
+
+  object Double
+  {
+    def apply(x: scala.Double): java.lang.String = x.toString
+    def unapply(s: java.lang.String): Option[scala.Double] =
+      try { Some(java.lang.Double.parseDouble(s)) }
+      catch { case _: NumberFormatException => None }
+    def parse(s: java.lang.String): scala.Double =
+      unapply(s) getOrElse error("Bad real: " + quote(s))
+  }
+}
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -183,6 +183,9 @@
     def is_quasi_command(token: Token): Boolean =
       token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
 
+    def is_indent_command(token: Token): Boolean =
+      token.is_begin_or_command || is_quasi_command(token)
+
 
     /* load commands */
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -217,7 +217,7 @@
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);
 val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
-val real = float_number >> Markup.parse_real || int >> Real.fromInt;
+val real = float_number >> Value.parse_real || int >> Real.fromInt;
 
 val tag_name = group (fn () => "tag name") (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -44,7 +44,7 @@
     | SOME 1 => pos
     | SOME j =>
         Position.properties_of pos
-        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
+        |> Properties.put (Markup.offsetN, Value.print_int (j - 1))
         |> Position.of_properties)
   end;
 
@@ -89,7 +89,7 @@
         is_reported pos ?
           let
             fun markup () =
-              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Markup.print_int id)]);
+              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]);
           in cons (pos, markup, fn () => "") end
       end;
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -35,24 +35,24 @@
       userCounters} = PolyML.Statistics.getLocalStats ();
     val user_counters =
       Vector.foldri
-        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
+        (fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
         [] userCounters;
   in
-    [("full_GCs", Markup.print_int gcFullGCs),
-     ("partial_GCs", Markup.print_int gcPartialGCs),
-     ("size_allocation", Markup.print_int sizeAllocation),
-     ("size_allocation_free", Markup.print_int sizeAllocationFree),
-     ("size_heap", Markup.print_int sizeHeap),
-     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
-     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
-     ("threads_in_ML", Markup.print_int threadsInML),
-     ("threads_total", Markup.print_int threadsTotal),
-     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
-     ("threads_wait_IO", Markup.print_int threadsWaitIO),
-     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
-     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
-     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
+    [("full_GCs", Value.print_int gcFullGCs),
+     ("partial_GCs", Value.print_int gcPartialGCs),
+     ("size_allocation", Value.print_int sizeAllocation),
+     ("size_allocation_free", Value.print_int sizeAllocationFree),
+     ("size_heap", Value.print_int sizeHeap),
+     ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
+     ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
+     ("threads_in_ML", Value.print_int threadsInML),
+     ("threads_total", Value.print_int threadsTotal),
+     ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
+     ("threads_wait_IO", Value.print_int threadsWaitIO),
+     ("threads_wait_mutex", Value.print_int threadsWaitMutex),
+     ("threads_wait_signal", Value.print_int threadsWaitSignal),
+     ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
     user_counters
   end;
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -14,8 +14,8 @@
   private def signed_int(s: String): String =
     if (s(0) == '-') "~" + s.substring(1) else s
 
-  def print_int(i: Int): String = signed_int(Properties.Value.Int(i))
-  def print_long(i: Long): String = signed_int(Properties.Value.Long(i))
+  def print_int(i: Int): String = signed_int(Value.Int(i))
+  def print_long(i: Long): String = signed_int(Value.Long(i))
 
 
   /* string */
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/document_id.ML
--- a/src/Pure/PIDE/document_id.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/document_id.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -31,8 +31,8 @@
 val none = 0;
 val make = Counter.make ();
 
-val parse = Markup.parse_int;
-val print = Markup.print_int;
+val parse = Value.parse_int;
+val print = Value.print_int;
 
 end;
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/document_id.scala
--- a/src/Pure/PIDE/document_id.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/document_id.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -20,7 +20,7 @@
   val none: Generic = 0
   val make = Counter.make()
 
-  def apply(id: Generic): String = Properties.Value.Long.apply(id)
-  def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
+  def apply(id: Generic): String = Value.Long.apply(id)
+  def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
 }
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -6,13 +6,6 @@
 
 signature MARKUP =
 sig
-  val parse_bool: string -> bool
-  val print_bool: bool -> string
-  val parse_nat: string -> int
-  val parse_int: string -> int
-  val print_int: int -> string
-  val parse_real: string -> real
-  val print_real: real -> string
   type T = string * Properties.T
   val empty: T
   val is_empty: T -> bool
@@ -228,45 +221,6 @@
 
 (** markup elements **)
 
-(* misc values *)
-
-fun parse_bool "true" = true
-  | parse_bool "false" = false
-  | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
-
-val print_bool = Bool.toString;
-
-
-fun parse_nat s =
-  let val i = Int.fromString s in
-    if is_none i orelse the i < 0
-    then raise Fail ("Bad natural number " ^ quote s)
-    else the i
-  end;
-
-fun parse_int s =
-  let val i = Int.fromString s in
-    if is_none i orelse String.isPrefix "~" s
-    then raise Fail ("Bad integer " ^ quote s)
-    else the i
-  end;
-
-val print_int = signed_string_of_int;
-
-
-fun parse_real s =
-  (case Real.fromString s of
-    SOME x => x
-  | NONE => raise Fail ("Bad real " ^ quote s));
-
-fun print_real x =
-  let val s = signed_string_of_real x in
-    (case space_explode "." s of
-      [a, b] => if forall_string (fn c => c = "0") b then a else s
-    | _ => s)
-  end;
-
-
 (* basic markup *)
 
 type T = string * Properties.T;
@@ -282,7 +236,7 @@
 
 fun markup_elem name = (name, (name, []): T);
 fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
-fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T);
+fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T);
 
 
 (* misc properties *)
@@ -293,7 +247,7 @@
 val kindN = "kind";
 
 val serialN = "serial";
-fun serial_properties i = [(serialN, print_int i)];
+fun serial_properties i = [(serialN, Value.print_int i)];
 
 val instanceN = "instance";
 
@@ -311,9 +265,9 @@
 fun language {name, symbols, antiquotes, delimited} =
   (languageN,
    [(nameN, name),
-    (symbolsN, print_bool symbols),
-    (antiquotesN, print_bool antiquotes),
-    (delimitedN, print_bool delimited)]);
+    (symbolsN, Value.print_bool symbols),
+    (antiquotesN, Value.print_bool antiquotes),
+    (delimitedN, Value.print_bool delimited)]);
 
 fun language' {name, symbols, antiquotes} delimited =
   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
@@ -412,14 +366,14 @@
 val blockN = "block";
 fun block c i =
   (blockN,
-    (if c then [(consistentN, print_bool c)] else []) @
-    (if i <> 0 then [(indentN, print_int i)] else []));
+    (if c then [(consistentN, Value.print_bool c)] else []) @
+    (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val breakN = "break";
 fun break w i =
   (breakN,
-    (if w <> 0 then [(widthN, print_int w)] else []) @
-    (if i <> 0 then [(indentN, print_int i)] else []));
+    (if w <> 0 then [(widthN, Value.print_int w)] else []) @
+    (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
@@ -520,7 +474,7 @@
 (* formal input *)
 
 val inputN = "input";
-fun input delimited props = (inputN, (delimitedN, print_bool delimited) :: props);
+fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props);
 
 
 (* outer syntax *)
@@ -565,13 +519,13 @@
 val command_timingN = "command_timing";
 
 fun command_timing_properties {file, offset, name} elapsed =
- [(fileN, file), (offsetN, print_int offset),
+ [(fileN, file), (offsetN, Value.print_int offset),
   (nameN, name), (elapsedN, Time.toString elapsed)];
 
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
-      SOME ({file = file, offset = parse_int offset, name = name},
+      SOME ({file = file, offset = Value.parse_int offset, name = name},
         Properties.seconds props elapsedN)
   | _ => NONE);
 
@@ -635,7 +589,7 @@
 val padding_command = (paddingN, "command");
 
 val dialogN = "dialog";
-fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
+fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]);
 
 val jedit_actionN = "jedit_action";
 
@@ -685,7 +639,7 @@
 val simp_trace_hintN = "simp_trace_hint";
 val simp_trace_ignoreN = "simp_trace_ignore";
 
-fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
+fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)];
 
 
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -113,7 +113,7 @@
 val _ =
   Isabelle_Process.protocol_command "Document.dialog_result"
     (fn [serial, result] =>
-      Active.dialog_result (Markup.parse_int serial) result
+      Active.dialog_result (Value.parse_int serial) result
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
 
 val _ =
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -404,7 +404,7 @@
   /* dialog via document content */
 
   def dialog_result(serial: Long, result: String): Unit =
-    protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
+    protocol_command("Document.dialog_result", Value.Long(serial), result)
 
 
   /* build_theories */
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -105,8 +105,8 @@
               case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
                 val props1 =
                   props.map({
-                    case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id =>
-                      (Markup.ID, Properties.Value.Long(command.id))
+                    case (Markup.ID, Value.Long(id)) if id == state0.exec_id =>
+                      (Markup.ID, Value.Long(command.id))
                     case p => p
                   })
                 XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/PIDE/xml.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -339,7 +339,7 @@
 (* atomic values *)
 
 fun int_atom s =
-  Markup.parse_int s
+  Value.parse_int s
     handle Fail _ => raise XML_ATOM s;
 
 fun bool_atom "0" = false
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Sep 06 21:36:48 2016 +0200
@@ -94,7 +94,9 @@
 abbrevs
   "default_sort" = ""
   "simproc_setup" = ""
+  "hence" = ""
   "hence" = "then have"
+  "thus" = ""
   "thus" = "then show"
   "apply_end" = ""
   "realizers" = ""
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -33,6 +33,7 @@
 ML_file "General/table.ML";
 
 ML_file "General/random.ML";
+ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -183,8 +183,8 @@
   in props end;
 
 val get_string = get_property "" I;
-val get_bool = get_property false Markup.parse_bool;
-val get_nat = get_property 0 Markup.parse_nat;
+val get_bool = get_property false Value.parse_bool;
+val get_nat = get_property 0 Value.parse_nat;
 
 end;
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/System/bash.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -124,7 +124,7 @@
           if (timing_file.isFile) {
             val t =
               Word.explode(File.read(timing_file)) match {
-                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
+                case List(Value.Long(elapsed), Value.Long(cpu)) =>
                   Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
                 case _ => Timing.zero
               }
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -81,7 +81,7 @@
             val _ =
               writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
                 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
-            val m = Markup.parse_int (Future.join promise)
+            val m = Value.parse_int (Future.join promise)
               handle Fail _ => error "Stopped";
           in
             Synchronized.change tracing_messages
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/System/options.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -114,15 +114,15 @@
 
 (* internal lookup and update *)
 
-val bool = get boolT (try Markup.parse_bool);
-val int = get intT (try Markup.parse_int);
-val real = get realT (try Markup.parse_real);
+val bool = get boolT (try Value.parse_bool);
+val int = get intT (try Value.parse_int);
+val real = get realT (try Value.parse_real);
 val seconds = Time.fromReal oo real;
 val string = get stringT SOME;
 
-val put_bool = put boolT Markup.print_bool;
-val put_int = put intT Markup.print_int;
-val put_real = put realT Markup.print_real;
+val put_bool = put boolT Value.print_bool;
+val put_int = put intT Value.print_int;
+val put_real = put realT Value.print_real;
 val put_string = put stringT I;
 
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/System/options.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -250,25 +250,25 @@
 
   class Bool_Access
   {
-    def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
+    def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
     def update(name: String, x: Boolean): Options =
-      put(name, Options.Bool, Properties.Value.Boolean(x))
+      put(name, Options.Bool, Value.Boolean(x))
   }
   val bool = new Bool_Access
 
   class Int_Access
   {
-    def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
+    def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
     def update(name: String, x: Int): Options =
-      put(name, Options.Int, Properties.Value.Int(x))
+      put(name, Options.Int, Value.Int(x))
   }
   val int = new Int_Access
 
   class Real_Access
   {
-    def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
+    def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
     def update(name: String, x: Double): Options =
-      put(name, Options.Real, Properties.Value.Double(x))
+      put(name, Options.Real, Value.Double(x))
   }
   val real = new Real_Access
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Thy/html.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -37,7 +37,7 @@
 fun make_symbols codes =
   let
     val mapping =
-      map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @
+      map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @
        [("'", "&#39;"),
         ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
         ("\<^esub>", hidden "&#8665;" ^ "</sub>"),
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -790,7 +790,7 @@
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/build_doc.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -88,7 +88,7 @@
   suitable document_variants entry.
 """,
       "a" -> (_ => all_docs = true),
-      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "s" -> (_ => system_mode = true))
 
     val docs = getopts(args)
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -38,8 +38,6 @@
 
   def parse(text: String): Build_Stats =
   {
-    import Properties.Value
-
     val ml_options = new mutable.ListBuffer[(String, String)]
     var finished = Map.empty[String, Timing]
     var timing = Map.empty[String, Timing]
@@ -208,11 +206,11 @@
         "D:" -> (arg => target_dir = Path.explode(arg)),
         "M" -> (_ => ml_timing = Some(true)),
         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
-        "T:" -> (arg => elapsed_threshold = Time.minutes(Properties.Value.Double.parse(arg))),
-        "l:" -> (arg => history_length = Properties.Value.Int.parse(arg)),
+        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
+        "l:" -> (arg => history_length = Value.Int.parse(arg)),
         "m" -> (_ => ml_timing = Some(false)),
         "s:" -> (arg =>
-          space_explode('x', arg).map(Properties.Value.Int.parse(_)) match {
+          space_explode('x', arg).map(Value.Int.parse(_)) match {
             case List(w, h) if w > 0 && h > 0 => size = (w, h)
             case _ => error("Error bad PNG image size: " + quote(arg))
           }))
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -217,10 +217,10 @@
   | ["step_out"] => (step_out (); false)
   | ["eval", index, SML, txt1, txt2] =>
      (error_wrapper (fn () =>
-        eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
+        eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true)
   | ["print_vals", index, SML, txt] =>
      (error_wrapper (fn () =>
-        print_vals thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt); true)
+        print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true)
   | bad =>
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
@@ -261,17 +261,17 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.break"
-    (fn [b] => set_break (Markup.parse_bool b));
+    (fn [b] => set_break (Value.parse_bool b));
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.breakpoint"
     (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
       let
-        val id = Markup.parse_int id0;
-        val breakpoint = Markup.parse_int breakpoint0;
-        val breakpoint_state = Markup.parse_bool breakpoint_state0;
+        val id = Value.parse_int id0;
+        val breakpoint = Value.parse_int breakpoint0;
+        val breakpoint_state = Value.parse_bool breakpoint_state0;
 
-        fun err () = error ("Bad exec for command " ^ Markup.print_int id);
+        fun err () = error ("Bad exec for command " ^ Value.print_int id);
       in
         (case Document.command_exec (Document.state ()) node_name id of
           SOME (eval, _) =>
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -234,8 +234,8 @@
         "Debugger.breakpoint",
         Symbol.encode(command.node_name.node),
         Document_ID(command.id),
-        Properties.Value.Long(breakpoint),
-        Properties.Value.Boolean(breakpoint_state))
+        Value.Long(breakpoint),
+        Value.Boolean(breakpoint_state))
       state1
     })
   }
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -180,8 +180,8 @@
         val {props = more_props, pretty} = payload ()
         val props =
           [(textN, text),
-           (memoryN, Markup.print_bool memory),
-           (parentN, Markup.print_int parent)]
+           (memoryN, Value.print_bool memory),
+           (parentN, Value.print_int parent)]
         val data =
           Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
       in
@@ -405,7 +405,7 @@
   Isabelle_Process.protocol_command "Simplifier_Trace.reply"
     (fn [serial_string, reply] =>
       let
-        val serial = Markup.parse_int serial_string
+        val serial = Value.parse_int serial_string
         val result =
           Synchronized.change_result futures
             (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -165,7 +165,7 @@
     def do_reply(session: Session, serial: Long, answer: Answer)
     {
       session.protocol_command(
-        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
+        "Simplifier_Trace.reply", Value.Long(serial), answer.name)
     }
 
     Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/build-jars	Tue Sep 06 21:36:48 2016 +0200
@@ -50,6 +50,7 @@
   General/timing.scala
   General/untyped.scala
   General/url.scala
+  General/value.scala
   General/word.scala
   General/xz_file.scala
   Isar/document_structure.scala
diff -r 761f81af2458 -r 5f8643e8ced5 src/Pure/config.ML
--- a/src/Pure/config.ML	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Pure/config.ML	Tue Sep 06 21:36:48 2016 +0200
@@ -44,7 +44,7 @@
 fun print_value (Bool true) = "true"
   | print_value (Bool false) = "false"
   | print_value (Int i) = signed_string_of_int i
-  | print_value (Real x) = Markup.print_real x
+  | print_value (Real x) = Value.print_real x
   | print_value (String s) = quote s;
 
 fun print_type (Bool _) = "bool"
@@ -103,7 +103,7 @@
 
 (* context information *)
 
-structure Value = Generic_Data
+structure Data = Generic_Data
 (
   type T = value Inttab.table;
   val empty = Inttab.empty;
@@ -116,12 +116,12 @@
     val id = serial ();
 
     fun get_value context =
-      (case Inttab.lookup (Value.get context) id of
+      (case Inttab.lookup (Data.get context) id of
         SOME value => value
       | NONE => default context);
 
     fun map_value f context =
-      Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
+      Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
   in
     Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
   end;
diff -r 761f81af2458 -r 5f8643e8ced5 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -284,12 +284,10 @@
             val (tokens1, context1) = line_content(line_range.start, caret, context0)
             val (tokens2, _) = line_content(caret, line_range.stop, context1)
 
-            if (tokens1.nonEmpty &&
-                (tokens1.head.is_begin_or_command || keywords.is_quasi_command(tokens1.head)))
+            if (tokens1.nonEmpty && keywords.is_indent_command(tokens1.head))
               buffer.indentLine(line, true)
 
-            if (tokens2.isEmpty ||
-                tokens2.head.is_begin_or_command || keywords.is_quasi_command(tokens2.head))
+            if (tokens2.isEmpty || keywords.is_indent_command(tokens2.head))
               JEdit_Lib.buffer_edit(buffer) {
                 text_area.setSelectedText("\n")
                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
diff -r 761f81af2458 -r 5f8643e8ced5 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -33,7 +33,7 @@
     statistics = statistics.enqueue(stats)
     statistics_length += 1
     limit_data.text match {
-      case Properties.Value.Int(limit) =>
+      case Value.Int(limit) =>
         while (statistics_length > limit) {
           statistics = statistics.dequeue._2
           statistics_length -= 1
@@ -91,7 +91,7 @@
   private val limit_data = new TextField("200", 5) {
     tooltip = "Limit for accumulated data"
     verifier = (s: String) =>
-      s match { case Properties.Value.Int(x) => x > 0 case _ => false }
+      s match { case Value.Int(x) => x > 0 case _ => false }
     reactions += { case ValueChanged(_) => input_delay.invoke() }
   }
 
diff -r 761f81af2458 -r 5f8643e8ced5 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -102,7 +102,7 @@
     private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
       tooltip = "Limit of displayed results"
       verifier = (s: String) =>
-        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+        s match { case Value.Int(x) => x >= 0 case _ => false }
       listenTo(keys)
       reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
     }
diff -r 761f81af2458 -r 5f8643e8ced5 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Sep 06 15:23:01 2016 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Sep 06 21:36:48 2016 +0200
@@ -132,14 +132,14 @@
     reactions += {
       case _: ValueChanged =>
         text match {
-          case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
+          case Value.Double(x) if x >= 0.0 => timing_threshold = x
           case _ =>
         }
         handle_update()
     }
     tooltip = threshold_tooltip
     verifier = ((s: String) =>
-      s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
+      s match { case Value.Double(x) => x >= 0.0 case _ => false })
   }
 
   private val controls =