clarified modules;
authorwenzelm
Mon Sep 05 23:11:00 2016 +0200 (2016-09-05)
changeset 63806c54a53ef1873
parent 63805 c272680df665
child 63807 5f77017055a3
clarified modules;
src/HOL/Code_Evaluation.thy
src/HOL/Library/code_test.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/value.ML
src/HOL/Tools/value_command.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_exn.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/position.ML
src/Pure/General/value.ML
src/Pure/Isar/parse.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_statistics.ML
src/Pure/PIDE/document_id.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/xml.ML
src/Pure/ROOT.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/options.ML
src/Pure/Thy/html.ML
src/Pure/Tools/debugger.ML
src/Pure/Tools/simplifier_trace.ML
src/Pure/config.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Sep 05 22:09:52 2016 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Sep 05 23:11:00 2016 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  
     1.5  code_reserved Eval Code_Evaluation
     1.6  
     1.7 -ML_file "~~/src/HOL/Tools/value.ML"
     1.8 +ML_file "~~/src/HOL/Tools/value_command.ML"
     1.9  
    1.10  
    1.11  subsection \<open>\<open>term_of\<close> instances\<close>
     2.1 --- a/src/HOL/Library/code_test.ML	Mon Sep 05 22:09:52 2016 +0200
     2.2 +++ b/src/HOL/Library/code_test.ML	Mon Sep 05 23:11:00 2016 +0200
     2.3 @@ -579,7 +579,7 @@
     2.4     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
     2.5     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
     2.6     (scalaN, (evaluate_in_scala, Code_Scala.target))]
     2.7 -  #> fold (fn target => Value.add_evaluator (target, eval_term target))
     2.8 +  #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
     2.9      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
    2.10  
    2.11  end
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 05 22:09:52 2016 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 05 23:11:00 2016 +0200
     3.3 @@ -626,7 +626,7 @@
     3.4              Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
     3.5            val trivial =
     3.6              if AList.lookup (op =) args check_trivialK |> the_default trivial_default
     3.7 -                            |> Markup.parse_bool then
     3.8 +                            |> Value.parse_bool then
     3.9                Try0.try0 (SOME try_timeout) ([], [], [], []) pre
    3.10                handle Timeout.TIMEOUT _ => false
    3.11              else false
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Sep 05 22:09:52 2016 +0200
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Sep 05 23:11:00 2016 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  fun get args name default_value =
     4.6    case AList.lookup (op =) args name of
     4.7 -    SOME value => Markup.parse_real value
     4.8 +    SOME value => Value.parse_real value
     4.9    | NONE => default_value
    4.10  
    4.11  fun extract_relevance_fudge args
     5.1 --- a/src/HOL/Tools/value.ML	Mon Sep 05 22:09:52 2016 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,87 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/value.ML
     5.5 -    Author:     Florian Haftmann, TU Muenchen
     5.6 -
     5.7 -Generic value command for arbitrary evaluators, with default using nbe or SML.
     5.8 -*)
     5.9 -
    5.10 -signature VALUE =
    5.11 -sig
    5.12 -  val value: Proof.context -> term -> term
    5.13 -  val value_select: string -> Proof.context -> term -> term
    5.14 -  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    5.15 -  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    5.16 -end;
    5.17 -
    5.18 -structure Value : VALUE =
    5.19 -struct
    5.20 -
    5.21 -fun default_value ctxt t =
    5.22 -  if null (Term.add_frees t [])
    5.23 -  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
    5.24 -    SOME t' => t'
    5.25 -  | NONE => Nbe.dynamic_value ctxt t
    5.26 -  else Nbe.dynamic_value ctxt t;
    5.27 -
    5.28 -structure Evaluator = Theory_Data
    5.29 -(
    5.30 -  type T = (string * (Proof.context -> term -> term)) list;
    5.31 -  val empty = [("default", default_value)];
    5.32 -  val extend = I;
    5.33 -  fun merge data : T = AList.merge (op =) (K true) data;
    5.34 -)
    5.35 -
    5.36 -val add_evaluator = Evaluator.map o AList.update (op =);
    5.37 -
    5.38 -fun value_select name ctxt =
    5.39 -  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    5.40 -   of NONE => error ("No such evaluator: " ^ name)
    5.41 -    | SOME f => f ctxt;
    5.42 -
    5.43 -fun value ctxt =
    5.44 -  let
    5.45 -    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    5.46 -  in
    5.47 -    if null evaluators
    5.48 -    then error "No evaluators"
    5.49 -    else (snd o snd o split_last) evaluators ctxt
    5.50 -  end;
    5.51 -
    5.52 -fun value_maybe_select some_name =
    5.53 -  case some_name
    5.54 -    of NONE => value
    5.55 -     | SOME name => value_select name;
    5.56 -  
    5.57 -fun value_cmd some_name modes raw_t state =
    5.58 -  let
    5.59 -    val ctxt = Toplevel.context_of state;
    5.60 -    val t = Syntax.read_term ctxt raw_t;
    5.61 -    val t' = value_maybe_select some_name ctxt t;
    5.62 -    val ty' = Term.type_of t';
    5.63 -    val ctxt' = Variable.auto_fixes t' ctxt;
    5.64 -    val p = Print_Mode.with_modes modes (fn () =>
    5.65 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    5.66 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    5.67 -  in Pretty.writeln p end;
    5.68 -
    5.69 -val opt_modes =
    5.70 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
    5.71 -
    5.72 -val opt_evaluator =
    5.73 -  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
    5.74 -  
    5.75 -val _ =
    5.76 -  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
    5.77 -    (opt_evaluator -- opt_modes -- Parse.term
    5.78 -      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
    5.79 -
    5.80 -val _ = Theory.setup
    5.81 -  (Thy_Output.antiquotation @{binding value}
    5.82 -    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    5.83 -    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    5.84 -      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    5.85 -        [style (value_maybe_select some_name context t)]))
    5.86 -  #> add_evaluator ("simp", Code_Simp.dynamic_value)
    5.87 -  #> add_evaluator ("nbe", Nbe.dynamic_value)
    5.88 -  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
    5.89 -
    5.90 -end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/value_command.ML	Mon Sep 05 23:11:00 2016 +0200
     6.3 @@ -0,0 +1,87 @@
     6.4 +(*  Title:      HOL/Tools/value_command.ML
     6.5 +    Author:     Florian Haftmann, TU Muenchen
     6.6 +
     6.7 +Generic value command for arbitrary evaluators, with default using nbe or SML.
     6.8 +*)
     6.9 +
    6.10 +signature VALUE_COMMAND =
    6.11 +sig
    6.12 +  val value: Proof.context -> term -> term
    6.13 +  val value_select: string -> Proof.context -> term -> term
    6.14 +  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    6.15 +  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    6.16 +end;
    6.17 +
    6.18 +structure Value_Command : VALUE_COMMAND =
    6.19 +struct
    6.20 +
    6.21 +fun default_value ctxt t =
    6.22 +  if null (Term.add_frees t [])
    6.23 +  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
    6.24 +    SOME t' => t'
    6.25 +  | NONE => Nbe.dynamic_value ctxt t
    6.26 +  else Nbe.dynamic_value ctxt t;
    6.27 +
    6.28 +structure Evaluator = Theory_Data
    6.29 +(
    6.30 +  type T = (string * (Proof.context -> term -> term)) list;
    6.31 +  val empty = [("default", default_value)];
    6.32 +  val extend = I;
    6.33 +  fun merge data : T = AList.merge (op =) (K true) data;
    6.34 +)
    6.35 +
    6.36 +val add_evaluator = Evaluator.map o AList.update (op =);
    6.37 +
    6.38 +fun value_select name ctxt =
    6.39 +  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    6.40 +   of NONE => error ("No such evaluator: " ^ name)
    6.41 +    | SOME f => f ctxt;
    6.42 +
    6.43 +fun value ctxt =
    6.44 +  let
    6.45 +    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    6.46 +  in
    6.47 +    if null evaluators
    6.48 +    then error "No evaluators"
    6.49 +    else (snd o snd o split_last) evaluators ctxt
    6.50 +  end;
    6.51 +
    6.52 +fun value_maybe_select some_name =
    6.53 +  case some_name
    6.54 +    of NONE => value
    6.55 +     | SOME name => value_select name;
    6.56 +  
    6.57 +fun value_cmd some_name modes raw_t state =
    6.58 +  let
    6.59 +    val ctxt = Toplevel.context_of state;
    6.60 +    val t = Syntax.read_term ctxt raw_t;
    6.61 +    val t' = value_maybe_select some_name ctxt t;
    6.62 +    val ty' = Term.type_of t';
    6.63 +    val ctxt' = Variable.auto_fixes t' ctxt;
    6.64 +    val p = Print_Mode.with_modes modes (fn () =>
    6.65 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    6.66 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    6.67 +  in Pretty.writeln p end;
    6.68 +
    6.69 +val opt_modes =
    6.70 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
    6.71 +
    6.72 +val opt_evaluator =
    6.73 +  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
    6.74 +  
    6.75 +val _ =
    6.76 +  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
    6.77 +    (opt_evaluator -- opt_modes -- Parse.term
    6.78 +      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
    6.79 +
    6.80 +val _ = Theory.setup
    6.81 +  (Thy_Output.antiquotation @{binding value}
    6.82 +    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    6.83 +    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    6.84 +      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    6.85 +        [style (value_maybe_select some_name context t)]))
    6.86 +  #> add_evaluator ("simp", Code_Simp.dynamic_value)
    6.87 +  #> add_evaluator ("nbe", Nbe.dynamic_value)
    6.88 +  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
    6.89 +
    6.90 +end;
     7.1 --- a/src/Pure/Concurrent/future.ML	Mon Sep 05 22:09:52 2016 +0200
     7.2 +++ b/src/Pure/Concurrent/future.ML	Mon Sep 05 23:11:00 2016 +0200
     7.3 @@ -171,15 +171,15 @@
     7.4        val active = count_workers Working;
     7.5        val waiting = count_workers Waiting;
     7.6        val stats =
     7.7 -       [("now", Markup.print_real (Time.toReal (Time.now ()))),
     7.8 -        ("tasks_ready", Markup.print_int ready),
     7.9 -        ("tasks_pending", Markup.print_int pending),
    7.10 -        ("tasks_running", Markup.print_int running),
    7.11 -        ("tasks_passive", Markup.print_int passive),
    7.12 -        ("tasks_urgent", Markup.print_int urgent),
    7.13 -        ("workers_total", Markup.print_int total),
    7.14 -        ("workers_active", Markup.print_int active),
    7.15 -        ("workers_waiting", Markup.print_int waiting)] @
    7.16 +       [("now", Value.print_real (Time.toReal (Time.now ()))),
    7.17 +        ("tasks_ready", Value.print_int ready),
    7.18 +        ("tasks_pending", Value.print_int pending),
    7.19 +        ("tasks_running", Value.print_int running),
    7.20 +        ("tasks_passive", Value.print_int passive),
    7.21 +        ("tasks_urgent", Value.print_int urgent),
    7.22 +        ("workers_total", Value.print_int total),
    7.23 +        ("workers_active", Value.print_int active),
    7.24 +        ("workers_waiting", Value.print_int waiting)] @
    7.25          ML_Statistics.get ();
    7.26      in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
    7.27    else ();
     8.1 --- a/src/Pure/Concurrent/par_exn.ML	Mon Sep 05 22:09:52 2016 +0200
     8.2 +++ b/src/Pure/Concurrent/par_exn.ML	Mon Sep 05 23:11:00 2016 +0200
     8.3 @@ -31,7 +31,7 @@
     8.4    in Exn_Properties.update (update_serial @ update_props) exn end;
     8.5  
     8.6  fun the_serial exn =
     8.7 -  Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
     8.8 +  Value.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
     8.9  
    8.10  val exn_ord = rev_order o int_ord o apply2 the_serial;
    8.11  
     9.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon Sep 05 22:09:52 2016 +0200
     9.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon Sep 05 23:11:00 2016 +0200
     9.3 @@ -152,8 +152,8 @@
     9.4        (case timing of NONE => timing_start | SOME var => Synchronized.value var);
     9.5      fun micros time = string_of_int (Time.toNanoseconds time div 1000);
     9.6    in
     9.7 -    [("now", Markup.print_real (Time.toReal (Time.now ()))),
     9.8 -     ("task_name", name), ("task_id", Markup.print_int id),
     9.9 +    [("now", Value.print_real (Time.toReal (Time.now ()))),
    9.10 +     ("task_name", name), ("task_id", Value.print_int id),
    9.11       ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
    9.12      Position.properties_of pos
    9.13    end;
    10.1 --- a/src/Pure/General/position.ML	Mon Sep 05 22:09:52 2016 +0200
    10.2 +++ b/src/Pure/General/position.ML	Mon Sep 05 23:11:00 2016 +0200
    10.3 @@ -137,7 +137,7 @@
    10.4  fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
    10.5  fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
    10.6  
    10.7 -fun parse_id pos = Option.map Markup.parse_int (get_id pos);
    10.8 +fun parse_id pos = Option.map Value.parse_int (get_id pos);
    10.9  
   10.10  
   10.11  (* markup properties *)
   10.12 @@ -145,7 +145,7 @@
   10.13  fun get props name =
   10.14    (case Properties.get props name of
   10.15      NONE => 0
   10.16 -  | SOME s => Markup.parse_int s);
   10.17 +  | SOME s => Value.parse_int s);
   10.18  
   10.19  fun of_properties props =
   10.20    make {line = get props Markup.lineN,
   10.21 @@ -153,7 +153,7 @@
   10.22      end_offset = get props Markup.end_offsetN,
   10.23      props = props};
   10.24  
   10.25 -fun value k i = if valid i then [(k, Markup.print_int i)] else [];
   10.26 +fun value k i = if valid i then [(k, Value.print_int i)] else [];
   10.27  
   10.28  fun properties_of (Pos ((i, j, k), props)) =
   10.29    value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
   10.30 @@ -161,8 +161,8 @@
   10.31  val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
   10.32  
   10.33  fun entity_properties_of def serial pos =
   10.34 -  if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
   10.35 -  else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
   10.36 +  if def then (Markup.defN, Value.print_int serial) :: properties_of pos
   10.37 +  else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
   10.38  
   10.39  fun default_properties default props =
   10.40    if exists (member (op =) Markup.position_properties o #1) props then props
   10.41 @@ -205,8 +205,8 @@
   10.42      val props = properties_of pos;
   10.43      val (s1, s2) =
   10.44        (case (line_of pos, file_of pos) of
   10.45 -        (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
   10.46 -      | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
   10.47 +        (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
   10.48 +      | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
   10.49        | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   10.50        | _ => if is_reported pos then ("", "\<here>") else ("", ""));
   10.51    in
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/General/value.ML	Mon Sep 05 23:11:00 2016 +0200
    11.3 @@ -0,0 +1,57 @@
    11.4 +(*  Title:      Pure/General/value.ML
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Plain values, represented as string.
    11.8 +*)
    11.9 +
   11.10 +signature VALUE =
   11.11 +sig
   11.12 +  val parse_bool: string -> bool
   11.13 +  val print_bool: bool -> string
   11.14 +  val parse_nat: string -> int
   11.15 +  val parse_int: string -> int
   11.16 +  val print_int: int -> string
   11.17 +  val parse_real: string -> real
   11.18 +  val print_real: real -> string
   11.19 +end;
   11.20 +
   11.21 +structure Value: VALUE =
   11.22 +struct
   11.23 +
   11.24 +fun parse_bool "true" = true
   11.25 +  | parse_bool "false" = false
   11.26 +  | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
   11.27 +
   11.28 +val print_bool = Bool.toString;
   11.29 +
   11.30 +
   11.31 +fun parse_nat s =
   11.32 +  let val i = Int.fromString s in
   11.33 +    if is_none i orelse the i < 0
   11.34 +    then raise Fail ("Bad natural number " ^ quote s)
   11.35 +    else the i
   11.36 +  end;
   11.37 +
   11.38 +fun parse_int s =
   11.39 +  let val i = Int.fromString s in
   11.40 +    if is_none i orelse String.isPrefix "~" s
   11.41 +    then raise Fail ("Bad integer " ^ quote s)
   11.42 +    else the i
   11.43 +  end;
   11.44 +
   11.45 +val print_int = signed_string_of_int;
   11.46 +
   11.47 +
   11.48 +fun parse_real s =
   11.49 +  (case Real.fromString s of
   11.50 +    SOME x => x
   11.51 +  | NONE => raise Fail ("Bad real " ^ quote s));
   11.52 +
   11.53 +fun print_real x =
   11.54 +  let val s = signed_string_of_real x in
   11.55 +    (case space_explode "." s of
   11.56 +      [a, b] => if forall_string (fn c => c = "0") b then a else s
   11.57 +    | _ => s)
   11.58 +  end;
   11.59 +
   11.60 +end;
    12.1 --- a/src/Pure/Isar/parse.ML	Mon Sep 05 22:09:52 2016 +0200
    12.2 +++ b/src/Pure/Isar/parse.ML	Mon Sep 05 23:11:00 2016 +0200
    12.3 @@ -217,7 +217,7 @@
    12.4  
    12.5  val nat = number >> (#1 o Library.read_int o Symbol.explode);
    12.6  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
    12.7 -val real = float_number >> Markup.parse_real || int >> Real.fromInt;
    12.8 +val real = float_number >> Value.parse_real || int >> Real.fromInt;
    12.9  
   12.10  val tag_name = group (fn () => "tag name") (short_ident || string);
   12.11  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
    13.1 --- a/src/Pure/ML/ml_compiler.ML	Mon Sep 05 22:09:52 2016 +0200
    13.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Sep 05 23:11:00 2016 +0200
    13.3 @@ -44,7 +44,7 @@
    13.4      | SOME 1 => pos
    13.5      | SOME j =>
    13.6          Position.properties_of pos
    13.7 -        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
    13.8 +        |> Properties.put (Markup.offsetN, Value.print_int (j - 1))
    13.9          |> Position.of_properties)
   13.10    end;
   13.11  
   13.12 @@ -89,7 +89,7 @@
   13.13          is_reported pos ?
   13.14            let
   13.15              fun markup () =
   13.16 -              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Markup.print_int id)]);
   13.17 +              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]);
   13.18            in cons (pos, markup, fn () => "") end
   13.19        end;
   13.20  
    14.1 --- a/src/Pure/ML/ml_statistics.ML	Mon Sep 05 22:09:52 2016 +0200
    14.2 +++ b/src/Pure/ML/ml_statistics.ML	Mon Sep 05 23:11:00 2016 +0200
    14.3 @@ -35,24 +35,24 @@
    14.4        userCounters} = PolyML.Statistics.getLocalStats ();
    14.5      val user_counters =
    14.6        Vector.foldri
    14.7 -        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
    14.8 +        (fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
    14.9          [] userCounters;
   14.10    in
   14.11 -    [("full_GCs", Markup.print_int gcFullGCs),
   14.12 -     ("partial_GCs", Markup.print_int gcPartialGCs),
   14.13 -     ("size_allocation", Markup.print_int sizeAllocation),
   14.14 -     ("size_allocation_free", Markup.print_int sizeAllocationFree),
   14.15 -     ("size_heap", Markup.print_int sizeHeap),
   14.16 -     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
   14.17 -     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
   14.18 -     ("threads_in_ML", Markup.print_int threadsInML),
   14.19 -     ("threads_total", Markup.print_int threadsTotal),
   14.20 -     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
   14.21 -     ("threads_wait_IO", Markup.print_int threadsWaitIO),
   14.22 -     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
   14.23 -     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
   14.24 -     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
   14.25 -     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
   14.26 +    [("full_GCs", Value.print_int gcFullGCs),
   14.27 +     ("partial_GCs", Value.print_int gcPartialGCs),
   14.28 +     ("size_allocation", Value.print_int sizeAllocation),
   14.29 +     ("size_allocation_free", Value.print_int sizeAllocationFree),
   14.30 +     ("size_heap", Value.print_int sizeHeap),
   14.31 +     ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
   14.32 +     ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
   14.33 +     ("threads_in_ML", Value.print_int threadsInML),
   14.34 +     ("threads_total", Value.print_int threadsTotal),
   14.35 +     ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
   14.36 +     ("threads_wait_IO", Value.print_int threadsWaitIO),
   14.37 +     ("threads_wait_mutex", Value.print_int threadsWaitMutex),
   14.38 +     ("threads_wait_signal", Value.print_int threadsWaitSignal),
   14.39 +     ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
   14.40 +     ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
   14.41      user_counters
   14.42    end;
   14.43  
    15.1 --- a/src/Pure/PIDE/document_id.ML	Mon Sep 05 22:09:52 2016 +0200
    15.2 +++ b/src/Pure/PIDE/document_id.ML	Mon Sep 05 23:11:00 2016 +0200
    15.3 @@ -31,8 +31,8 @@
    15.4  val none = 0;
    15.5  val make = Counter.make ();
    15.6  
    15.7 -val parse = Markup.parse_int;
    15.8 -val print = Markup.print_int;
    15.9 +val parse = Value.parse_int;
   15.10 +val print = Value.print_int;
   15.11  
   15.12  end;
   15.13  
    16.1 --- a/src/Pure/PIDE/markup.ML	Mon Sep 05 22:09:52 2016 +0200
    16.2 +++ b/src/Pure/PIDE/markup.ML	Mon Sep 05 23:11:00 2016 +0200
    16.3 @@ -6,13 +6,6 @@
    16.4  
    16.5  signature MARKUP =
    16.6  sig
    16.7 -  val parse_bool: string -> bool
    16.8 -  val print_bool: bool -> string
    16.9 -  val parse_nat: string -> int
   16.10 -  val parse_int: string -> int
   16.11 -  val print_int: int -> string
   16.12 -  val parse_real: string -> real
   16.13 -  val print_real: real -> string
   16.14    type T = string * Properties.T
   16.15    val empty: T
   16.16    val is_empty: T -> bool
   16.17 @@ -228,45 +221,6 @@
   16.18  
   16.19  (** markup elements **)
   16.20  
   16.21 -(* misc values *)
   16.22 -
   16.23 -fun parse_bool "true" = true
   16.24 -  | parse_bool "false" = false
   16.25 -  | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
   16.26 -
   16.27 -val print_bool = Bool.toString;
   16.28 -
   16.29 -
   16.30 -fun parse_nat s =
   16.31 -  let val i = Int.fromString s in
   16.32 -    if is_none i orelse the i < 0
   16.33 -    then raise Fail ("Bad natural number " ^ quote s)
   16.34 -    else the i
   16.35 -  end;
   16.36 -
   16.37 -fun parse_int s =
   16.38 -  let val i = Int.fromString s in
   16.39 -    if is_none i orelse String.isPrefix "~" s
   16.40 -    then raise Fail ("Bad integer " ^ quote s)
   16.41 -    else the i
   16.42 -  end;
   16.43 -
   16.44 -val print_int = signed_string_of_int;
   16.45 -
   16.46 -
   16.47 -fun parse_real s =
   16.48 -  (case Real.fromString s of
   16.49 -    SOME x => x
   16.50 -  | NONE => raise Fail ("Bad real " ^ quote s));
   16.51 -
   16.52 -fun print_real x =
   16.53 -  let val s = signed_string_of_real x in
   16.54 -    (case space_explode "." s of
   16.55 -      [a, b] => if forall_string (fn c => c = "0") b then a else s
   16.56 -    | _ => s)
   16.57 -  end;
   16.58 -
   16.59 -
   16.60  (* basic markup *)
   16.61  
   16.62  type T = string * Properties.T;
   16.63 @@ -282,7 +236,7 @@
   16.64  
   16.65  fun markup_elem name = (name, (name, []): T);
   16.66  fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
   16.67 -fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T);
   16.68 +fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T);
   16.69  
   16.70  
   16.71  (* misc properties *)
   16.72 @@ -293,7 +247,7 @@
   16.73  val kindN = "kind";
   16.74  
   16.75  val serialN = "serial";
   16.76 -fun serial_properties i = [(serialN, print_int i)];
   16.77 +fun serial_properties i = [(serialN, Value.print_int i)];
   16.78  
   16.79  val instanceN = "instance";
   16.80  
   16.81 @@ -311,9 +265,9 @@
   16.82  fun language {name, symbols, antiquotes, delimited} =
   16.83    (languageN,
   16.84     [(nameN, name),
   16.85 -    (symbolsN, print_bool symbols),
   16.86 -    (antiquotesN, print_bool antiquotes),
   16.87 -    (delimitedN, print_bool delimited)]);
   16.88 +    (symbolsN, Value.print_bool symbols),
   16.89 +    (antiquotesN, Value.print_bool antiquotes),
   16.90 +    (delimitedN, Value.print_bool delimited)]);
   16.91  
   16.92  fun language' {name, symbols, antiquotes} delimited =
   16.93    language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
   16.94 @@ -412,14 +366,14 @@
   16.95  val blockN = "block";
   16.96  fun block c i =
   16.97    (blockN,
   16.98 -    (if c then [(consistentN, print_bool c)] else []) @
   16.99 -    (if i <> 0 then [(indentN, print_int i)] else []));
  16.100 +    (if c then [(consistentN, Value.print_bool c)] else []) @
  16.101 +    (if i <> 0 then [(indentN, Value.print_int i)] else []));
  16.102  
  16.103  val breakN = "break";
  16.104  fun break w i =
  16.105    (breakN,
  16.106 -    (if w <> 0 then [(widthN, print_int w)] else []) @
  16.107 -    (if i <> 0 then [(indentN, print_int i)] else []));
  16.108 +    (if w <> 0 then [(widthN, Value.print_int w)] else []) @
  16.109 +    (if i <> 0 then [(indentN, Value.print_int i)] else []));
  16.110  
  16.111  val (fbreakN, fbreak) = markup_elem "fbreak";
  16.112  
  16.113 @@ -520,7 +474,7 @@
  16.114  (* formal input *)
  16.115  
  16.116  val inputN = "input";
  16.117 -fun input delimited props = (inputN, (delimitedN, print_bool delimited) :: props);
  16.118 +fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props);
  16.119  
  16.120  
  16.121  (* outer syntax *)
  16.122 @@ -565,13 +519,13 @@
  16.123  val command_timingN = "command_timing";
  16.124  
  16.125  fun command_timing_properties {file, offset, name} elapsed =
  16.126 - [(fileN, file), (offsetN, print_int offset),
  16.127 + [(fileN, file), (offsetN, Value.print_int offset),
  16.128    (nameN, name), (elapsedN, Time.toString elapsed)];
  16.129  
  16.130  fun parse_command_timing_properties props =
  16.131    (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
  16.132      (SOME file, SOME offset, SOME name) =>
  16.133 -      SOME ({file = file, offset = parse_int offset, name = name},
  16.134 +      SOME ({file = file, offset = Value.parse_int offset, name = name},
  16.135          Properties.seconds props elapsedN)
  16.136    | _ => NONE);
  16.137  
  16.138 @@ -635,7 +589,7 @@
  16.139  val padding_command = (paddingN, "command");
  16.140  
  16.141  val dialogN = "dialog";
  16.142 -fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
  16.143 +fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]);
  16.144  
  16.145  val jedit_actionN = "jedit_action";
  16.146  
  16.147 @@ -685,7 +639,7 @@
  16.148  val simp_trace_hintN = "simp_trace_hint";
  16.149  val simp_trace_ignoreN = "simp_trace_ignore";
  16.150  
  16.151 -fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
  16.152 +fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)];
  16.153  
  16.154  
  16.155  
    17.1 --- a/src/Pure/PIDE/protocol.ML	Mon Sep 05 22:09:52 2016 +0200
    17.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Sep 05 23:11:00 2016 +0200
    17.3 @@ -113,7 +113,7 @@
    17.4  val _ =
    17.5    Isabelle_Process.protocol_command "Document.dialog_result"
    17.6      (fn [serial, result] =>
    17.7 -      Active.dialog_result (Markup.parse_int serial) result
    17.8 +      Active.dialog_result (Value.parse_int serial) result
    17.9          handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
   17.10  
   17.11  val _ =
    18.1 --- a/src/Pure/PIDE/xml.ML	Mon Sep 05 22:09:52 2016 +0200
    18.2 +++ b/src/Pure/PIDE/xml.ML	Mon Sep 05 23:11:00 2016 +0200
    18.3 @@ -339,7 +339,7 @@
    18.4  (* atomic values *)
    18.5  
    18.6  fun int_atom s =
    18.7 -  Markup.parse_int s
    18.8 +  Value.parse_int s
    18.9      handle Fail _ => raise XML_ATOM s;
   18.10  
   18.11  fun bool_atom "0" = false
    19.1 --- a/src/Pure/ROOT.ML	Mon Sep 05 22:09:52 2016 +0200
    19.2 +++ b/src/Pure/ROOT.ML	Mon Sep 05 23:11:00 2016 +0200
    19.3 @@ -33,6 +33,7 @@
    19.4  ML_file "General/table.ML";
    19.5  
    19.6  ML_file "General/random.ML";
    19.7 +ML_file "General/value.ML";
    19.8  ML_file "General/properties.ML";
    19.9  ML_file "General/output.ML";
   19.10  ML_file "PIDE/markup.ML";
    20.1 --- a/src/Pure/Syntax/syntax_ext.ML	Mon Sep 05 22:09:52 2016 +0200
    20.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Mon Sep 05 23:11:00 2016 +0200
    20.3 @@ -183,8 +183,8 @@
    20.4    in props end;
    20.5  
    20.6  val get_string = get_property "" I;
    20.7 -val get_bool = get_property false Markup.parse_bool;
    20.8 -val get_nat = get_property 0 Markup.parse_nat;
    20.9 +val get_bool = get_property false Value.parse_bool;
   20.10 +val get_nat = get_property 0 Value.parse_nat;
   20.11  
   20.12  end;
   20.13  
    21.1 --- a/src/Pure/System/isabelle_process.ML	Mon Sep 05 22:09:52 2016 +0200
    21.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Sep 05 23:11:00 2016 +0200
    21.3 @@ -81,7 +81,7 @@
    21.4              val _ =
    21.5                writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
    21.6                  text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
    21.7 -            val m = Markup.parse_int (Future.join promise)
    21.8 +            val m = Value.parse_int (Future.join promise)
    21.9                handle Fail _ => error "Stopped";
   21.10            in
   21.11              Synchronized.change tracing_messages
    22.1 --- a/src/Pure/System/options.ML	Mon Sep 05 22:09:52 2016 +0200
    22.2 +++ b/src/Pure/System/options.ML	Mon Sep 05 23:11:00 2016 +0200
    22.3 @@ -114,15 +114,15 @@
    22.4  
    22.5  (* internal lookup and update *)
    22.6  
    22.7 -val bool = get boolT (try Markup.parse_bool);
    22.8 -val int = get intT (try Markup.parse_int);
    22.9 -val real = get realT (try Markup.parse_real);
   22.10 +val bool = get boolT (try Value.parse_bool);
   22.11 +val int = get intT (try Value.parse_int);
   22.12 +val real = get realT (try Value.parse_real);
   22.13  val seconds = Time.fromReal oo real;
   22.14  val string = get stringT SOME;
   22.15  
   22.16 -val put_bool = put boolT Markup.print_bool;
   22.17 -val put_int = put intT Markup.print_int;
   22.18 -val put_real = put realT Markup.print_real;
   22.19 +val put_bool = put boolT Value.print_bool;
   22.20 +val put_int = put intT Value.print_int;
   22.21 +val put_real = put realT Value.print_real;
   22.22  val put_string = put stringT I;
   22.23  
   22.24  
    23.1 --- a/src/Pure/Thy/html.ML	Mon Sep 05 22:09:52 2016 +0200
    23.2 +++ b/src/Pure/Thy/html.ML	Mon Sep 05 23:11:00 2016 +0200
    23.3 @@ -37,7 +37,7 @@
    23.4  fun make_symbols codes =
    23.5    let
    23.6      val mapping =
    23.7 -      map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @
    23.8 +      map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @
    23.9         [("'", "&#39;"),
   23.10          ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
   23.11          ("\<^esub>", hidden "&#8665;" ^ "</sub>"),
    24.1 --- a/src/Pure/Tools/debugger.ML	Mon Sep 05 22:09:52 2016 +0200
    24.2 +++ b/src/Pure/Tools/debugger.ML	Mon Sep 05 23:11:00 2016 +0200
    24.3 @@ -217,10 +217,10 @@
    24.4    | ["step_out"] => (step_out (); false)
    24.5    | ["eval", index, SML, txt1, txt2] =>
    24.6       (error_wrapper (fn () =>
    24.7 -        eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
    24.8 +        eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true)
    24.9    | ["print_vals", index, SML, txt] =>
   24.10       (error_wrapper (fn () =>
   24.11 -        print_vals thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt); true)
   24.12 +        print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true)
   24.13    | bad =>
   24.14       (Output.system_message
   24.15          ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
   24.16 @@ -261,17 +261,17 @@
   24.17  
   24.18  val _ =
   24.19    Isabelle_Process.protocol_command "Debugger.break"
   24.20 -    (fn [b] => set_break (Markup.parse_bool b));
   24.21 +    (fn [b] => set_break (Value.parse_bool b));
   24.22  
   24.23  val _ =
   24.24    Isabelle_Process.protocol_command "Debugger.breakpoint"
   24.25      (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
   24.26        let
   24.27 -        val id = Markup.parse_int id0;
   24.28 -        val breakpoint = Markup.parse_int breakpoint0;
   24.29 -        val breakpoint_state = Markup.parse_bool breakpoint_state0;
   24.30 +        val id = Value.parse_int id0;
   24.31 +        val breakpoint = Value.parse_int breakpoint0;
   24.32 +        val breakpoint_state = Value.parse_bool breakpoint_state0;
   24.33  
   24.34 -        fun err () = error ("Bad exec for command " ^ Markup.print_int id);
   24.35 +        fun err () = error ("Bad exec for command " ^ Value.print_int id);
   24.36        in
   24.37          (case Document.command_exec (Document.state ()) node_name id of
   24.38            SOME (eval, _) =>
    25.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Sep 05 22:09:52 2016 +0200
    25.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Sep 05 23:11:00 2016 +0200
    25.3 @@ -180,8 +180,8 @@
    25.4          val {props = more_props, pretty} = payload ()
    25.5          val props =
    25.6            [(textN, text),
    25.7 -           (memoryN, Markup.print_bool memory),
    25.8 -           (parentN, Markup.print_int parent)]
    25.9 +           (memoryN, Value.print_bool memory),
   25.10 +           (parentN, Value.print_int parent)]
   25.11          val data =
   25.12            Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
   25.13        in
   25.14 @@ -405,7 +405,7 @@
   25.15    Isabelle_Process.protocol_command "Simplifier_Trace.reply"
   25.16      (fn [serial_string, reply] =>
   25.17        let
   25.18 -        val serial = Markup.parse_int serial_string
   25.19 +        val serial = Value.parse_int serial_string
   25.20          val result =
   25.21            Synchronized.change_result futures
   25.22              (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
    26.1 --- a/src/Pure/config.ML	Mon Sep 05 22:09:52 2016 +0200
    26.2 +++ b/src/Pure/config.ML	Mon Sep 05 23:11:00 2016 +0200
    26.3 @@ -44,7 +44,7 @@
    26.4  fun print_value (Bool true) = "true"
    26.5    | print_value (Bool false) = "false"
    26.6    | print_value (Int i) = signed_string_of_int i
    26.7 -  | print_value (Real x) = Markup.print_real x
    26.8 +  | print_value (Real x) = Value.print_real x
    26.9    | print_value (String s) = quote s;
   26.10  
   26.11  fun print_type (Bool _) = "bool"
   26.12 @@ -103,7 +103,7 @@
   26.13  
   26.14  (* context information *)
   26.15  
   26.16 -structure Value = Generic_Data
   26.17 +structure Data = Generic_Data
   26.18  (
   26.19    type T = value Inttab.table;
   26.20    val empty = Inttab.empty;
   26.21 @@ -116,12 +116,12 @@
   26.22      val id = serial ();
   26.23  
   26.24      fun get_value context =
   26.25 -      (case Inttab.lookup (Value.get context) id of
   26.26 +      (case Inttab.lookup (Data.get context) id of
   26.27          SOME value => value
   26.28        | NONE => default context);
   26.29  
   26.30      fun map_value f context =
   26.31 -      Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
   26.32 +      Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
   26.33    in
   26.34      Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
   26.35    end;