clarified modules;

--- a/src/HOL/Code_Evaluation.thy	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Sep 05 23:11:00 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>

--- a/src/HOL/Library/code_test.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/HOL/Library/code_test.ML	Mon Sep 05 23:11:00 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

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 05 23:11:00 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

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Sep 05 23:11:00 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

--- a/src/HOL/Tools/value.ML	Mon Sep 05 22:09:52 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;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/value_command.ML	Mon Sep 05 23:11:00 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;

--- a/src/Pure/Concurrent/future.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Sep 05 23:11:00 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 ();

--- a/src/Pure/Concurrent/par_exn.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Mon Sep 05 23:11:00 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;
 

--- a/src/Pure/Concurrent/task_queue.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Sep 05 23:11:00 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;

--- a/src/Pure/General/position.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/General/position.ML	Mon Sep 05 23:11:00 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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/value.ML	Mon Sep 05 23:11:00 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;

--- a/src/Pure/Isar/parse.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Sep 05 23:11:00 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);

--- a/src/Pure/ML/ml_compiler.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Sep 05 23:11:00 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;
 

--- a/src/Pure/ML/ml_statistics.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Mon Sep 05 23:11:00 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;
 

--- a/src/Pure/PIDE/document_id.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/PIDE/document_id.ML	Mon Sep 05 23:11:00 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;
 

--- a/src/Pure/PIDE/markup.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 05 23:11:00 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)];
 
 
 

--- a/src/Pure/PIDE/protocol.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Sep 05 23:11:00 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 _ =

--- a/src/Pure/PIDE/xml.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/PIDE/xml.ML	Mon Sep 05 23:11:00 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

--- a/src/Pure/ROOT.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 05 23:11:00 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";

--- a/src/Pure/Syntax/syntax_ext.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Mon Sep 05 23:11:00 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;
 

--- a/src/Pure/System/isabelle_process.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Sep 05 23:11:00 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

--- a/src/Pure/System/options.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/System/options.ML	Mon Sep 05 23:11:00 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;
 
 

--- a/src/Pure/Thy/html.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Thy/html.ML	Mon Sep 05 23:11:00 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 @
        [("'", "'"),
         ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
         ("\<^esub>", hidden "&#8665;" ^ "</sub>"),

--- a/src/Pure/Tools/debugger.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Sep 05 23:11:00 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, _) =>

--- a/src/Pure/Tools/simplifier_trace.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon Sep 05 23:11:00 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))

--- a/src/Pure/config.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/config.ML	Mon Sep 05 23:11:00 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;