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