# HG changeset patch # User wenzelm # Date 1473109860 -7200 # Node ID c54a53ef18730d183600fa786eae8153e48e93ad # Parent c272680df665842e6d094a240199d8fdf9bf02b1 clarified modules; diff -r c272680df665 -r c54a53ef1873 src/HOL/Code_Evaluation.thy --- 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 \\term_of\ instances\ diff -r c272680df665 -r c54a53ef1873 src/HOL/Library/code_test.ML --- 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 diff -r c272680df665 -r c54a53ef1873 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r c272680df665 -r c54a53ef1873 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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 diff -r c272680df665 -r c54a53ef1873 src/HOL/Tools/value.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/HOL/Tools/value_command.ML --- /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; diff -r c272680df665 -r c54a53ef1873 src/Pure/Concurrent/future.ML --- 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 (); diff -r c272680df665 -r c54a53ef1873 src/Pure/Concurrent/par_exn.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/Pure/Concurrent/task_queue.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/Pure/General/position.ML --- 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 ("", "\") else ("", "")); in diff -r c272680df665 -r c54a53ef1873 src/Pure/General/value.ML --- /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; diff -r c272680df665 -r c54a53ef1873 src/Pure/Isar/parse.ML --- 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); diff -r c272680df665 -r c54a53ef1873 src/Pure/ML/ml_compiler.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/Pure/ML/ml_statistics.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/Pure/PIDE/document_id.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/Pure/PIDE/markup.ML --- 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)]; diff -r c272680df665 -r c54a53ef1873 src/Pure/PIDE/protocol.ML --- 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 _ = diff -r c272680df665 -r c54a53ef1873 src/Pure/PIDE/xml.ML --- 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 diff -r c272680df665 -r c54a53ef1873 src/Pure/ROOT.ML --- 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"; diff -r c272680df665 -r c54a53ef1873 src/Pure/Syntax/syntax_ext.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; diff -r c272680df665 -r c54a53ef1873 src/Pure/System/isabelle_process.ML --- 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 diff -r c272680df665 -r c54a53ef1873 src/Pure/System/options.ML --- 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; diff -r c272680df665 -r c54a53ef1873 src/Pure/Thy/html.ML --- 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 "⇘" ^ ""), ("\<^esub>", hidden "⇙" ^ ""), diff -r c272680df665 -r c54a53ef1873 src/Pure/Tools/debugger.ML --- 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, _) => diff -r c272680df665 -r c54a53ef1873 src/Pure/Tools/simplifier_trace.ML --- 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)) diff -r c272680df665 -r c54a53ef1873 src/Pure/config.ML --- 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;