--- a/lib/texinputs/isabelle.sty Wed Sep 12 12:43:34 2012 +0200
+++ b/lib/texinputs/isabelle.sty Wed Sep 12 15:01:25 2012 +0200
@@ -103,9 +103,6 @@
\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
}
-\newcommand{\isaliteral}[2]{#2}
-\newcommand{\isanil}{}
-
% keyword and section markup
@@ -158,9 +155,9 @@
\isachardefaults%
\def\isacharunderscorekeyword{\mbox{-}}%
\def\isacharbang{\isamath{!}}%
-\def\isachardoublequote{\isanil}%
-\def\isachardoublequoteopen{\isanil}%
-\def\isachardoublequoteclose{\isanil}%
+\def\isachardoublequote{}%
+\def\isachardoublequoteopen{}%
+\def\isachardoublequoteclose{}%
\def\isacharhash{\isamath{\#}}%
\def\isachardollar{\isamath{\$}}%
\def\isacharpercent{\isamath{\%}}%
--- a/src/Doc/Functions/Functions.thy Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/Functions/Functions.thy Wed Sep 12 15:01:25 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Doc/Functions/Thy/Fundefs.thy
+(* Title: Doc/Functions/Fundefs.thy
Author: Alexander Krauss, TU Muenchen
Tutorial for function definitions with the new "function" package.
--- a/src/Doc/IsarRef/document/build Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/IsarRef/document/build Wed Sep 12 15:01:25 2012 +0200
@@ -11,7 +11,6 @@
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
-cp "$ISABELLE_HOME/src/Doc/isar.sty" .
cp "$ISABELLE_HOME/src/Doc/underscore.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
--- a/src/Doc/ROOT Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/ROOT Wed Sep 12 15:01:25 2012 +0200
@@ -5,6 +5,11 @@
files
"../prepare_document"
"../pdfsetup.sty"
+ "../iman.sty"
+ "../extra.sty"
+ "../isar.sty"
+ "../proof.sty"
+ "../manual.bib"
"document/build"
"document/root.tex"
"document/style.sty"
@@ -23,6 +28,11 @@
files
"../prepare_document"
"../pdfsetup.sty"
+ "../iman.sty"
+ "../extra.sty"
+ "../isar.sty"
+ "../proof.sty"
+ "../manual.bib"
"document/adapt.tex"
"document/architecture.tex"
"document/build"
@@ -80,8 +90,8 @@
"../extra.sty"
"../isar.sty"
"../proof.sty"
+ "../ttbox.sty"
"../underscore.sty"
- "../ttbox.sty"
"../manual.bib"
"document/build"
"document/root.tex"
@@ -110,9 +120,9 @@
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
+ "../isar.sty"
"../ttbox.sty"
- "../proof.sty"
- "../isar.sty"
+ "../underscore.sty"
"../manual.bib"
"document/build"
"document/isar-vm.eps"
@@ -285,8 +295,8 @@
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
+ "../isar.sty"
"../ttbox.sty"
- "../isar.sty"
"../underscore.sty"
"../manual.bib"
"document/browser_screenshot.eps"
--- a/src/Doc/Tutorial/Protocol/Event.thy Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/Tutorial/Protocol/Event.thy Wed Sep 12 15:01:25 2012 +0200
@@ -1,5 +1,4 @@
-(* Title: HOL/Auth/Event
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Datatype of events; function "spies"; freshness
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Wed Sep 12 15:01:25 2012 +0200
@@ -1,5 +1,4 @@
-(* Title: HOL/Auth/Message
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Datatypes of agents and messages;
--- a/src/Doc/Tutorial/Protocol/NS_Public.thy Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/Tutorial/Protocol/NS_Public.thy Wed Sep 12 15:01:25 2012 +0200
@@ -1,5 +1,4 @@
-(* Title: HOL/Auth/NS_Public
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
--- a/src/Doc/pdfsetup.sty Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Doc/pdfsetup.sty Wed Sep 12 15:01:25 2012 +0200
@@ -15,13 +15,3 @@
\urlstyle{rm}
\ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
-\def\isaliteral#1#2{#2}
-\def\isanil{}
-
-%experimental treatment of replacement text
-\iffalse
-\ifnum\pdfminorversion<5\pdfminorversion=5\fi
-\renewcommand{\isaliteral}[2]{%
-\pdfliteral direct{/Span <</ActualText<#1>>> BDC}#2\pdfliteral direct{EMC}}
-\renewcommand{\isanil}{{\color{white}.}}
-\fi
--- a/src/HOL/Library/Prefix_Order.thy Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/Library/Prefix_Order.thy Wed Sep 12 15:01:25 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Sublist.thy
+(* Title: HOL/Library/Prefix_Order.thy
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
*)
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Sep 12 15:01:25 2012 +0200
@@ -316,8 +316,8 @@
fun body 0 t = t
| body n t = body (n - 1) (t $ (Bound (n - 1)))
in
- body n (Const (str, Term.dummyT))
- |> funpow n (Term.absdummy Term.dummyT)
+ body n (Const (str, dummyT))
+ |> funpow n (Term.absdummy dummyT)
end
fun mk_fun_type [] b acc = acc b
| mk_fun_type (ty :: tys) b acc =
@@ -365,10 +365,10 @@
(string_of_interpreted_symbol interpreted_symbol))), [])
| Interpreted_Logic logic_symbol =>
(case logic_symbol of
- Equals => HOLogic.eq_const Term.dummyT
+ Equals => HOLogic.eq_const dummyT
| NEquals =>
- HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0)
- |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
+ HOLogic.mk_not (HOLogic.eq_const dummyT $ Bound 1 $ Bound 0)
+ |> (Term.absdummy dummyT #> Term.absdummy dummyT)
| Or => HOLogic.disj
| And => HOLogic.conj
| Iff => HOLogic.eq_const HOLogic.boolT
@@ -380,8 +380,8 @@
| Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}
| Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}
| Not => HOLogic.Not
- | Op_Forall => HOLogic.all_const Term.dummyT
- | Op_Exists => HOLogic.exists_const Term.dummyT
+ | Op_Forall => HOLogic.all_const dummyT
+ | Op_Exists => HOLogic.exists_const dummyT
| True => @{term "True"}
| False => @{term "False"}
)
@@ -404,7 +404,7 @@
fun mtimes thy =
fold (fn x => fn y =>
Sign.mk_const thy
- ("Product_Type.Pair", [Term.dummyT, Term.dummyT]) $ y $ x)
+ ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
fun mtimes' (args, thy) f =
let
@@ -530,7 +530,7 @@
SOME ty =>
(case ty of
SOME ty => Free (n, ty)
- | NONE => Free (n, Term.dummyT) (*to infer the variable's type*)
+ | NONE => Free (n, dummyT) (*to infer the variable's type*)
)
| NONE =>
raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
@@ -621,7 +621,7 @@
case ty of
NONE =>
f (n,
- if language = THF then Term.dummyT
+ if language = THF then dummyT
else
interpret_type config thy type_map
(Defined_type Type_Ind),
@@ -646,12 +646,12 @@
let val (t, thy') =
interpret_formula config language const_map var_types type_map
(Quant (Lambda, bindings, tptp_formula)) thy
- in ((HOLogic.choice_const Term.dummyT) $ t, thy') end
+ in ((HOLogic.choice_const dummyT) $ t, thy') end
| Iota =>
let val (t, thy') =
interpret_formula config language const_map var_types type_map
(Quant (Lambda, bindings, tptp_formula)) thy
- in (Const (@{const_name The}, Term.dummyT) $ t, thy') end
+ in (Const (@{const_name The}, dummyT) $ t, thy') end
| Dep_Prod =>
raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
| Dep_Sum =>
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Sep 12 15:01:25 2012 +0200
@@ -380,7 +380,7 @@
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
local
- val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
+ val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
fun default c = const_prefix ^ lookup_const c
in
fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 12 15:01:25 2012 +0200
@@ -38,7 +38,7 @@
end
fun pred_of_function thy name =
- case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
+ case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
[] => NONE
| [(f, p)] => SOME (fst (dest_Const p))
| _ => error ("Multiple matches possible for lookup of constant " ^ name)
--- a/src/HOL/Tools/inductive.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Sep 12 15:01:25 2012 +0200
@@ -49,7 +49,7 @@
(binding * string option * mixfix) list ->
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
- bool -> local_theory -> inductive_result * local_theory
+ local_theory -> inductive_result * local_theory
val add_inductive_global: inductive_flags ->
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
@@ -81,8 +81,8 @@
(binding * string option * mixfix) list ->
(binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
- bool -> local_theory -> inductive_result * local_theory
- val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
+ local_theory -> inductive_result * local_theory
+ val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
end;
structure Inductive: INDUCTIVE =
@@ -1039,7 +1039,7 @@
||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
end;
-fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
+fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
let
val ((vars, intrs), _) = lthy
|> Proof_Context.set_mode Proof_Context.mode_abbrev
@@ -1143,16 +1143,16 @@
Scan.optional Parse_Spec.where_alt_specs [] --
Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((preds, params), specs), monos) =>
- (snd oo gen_add_inductive mk_def true coind preds params specs monos));
+ (snd o gen_add_inductive mk_def true coind preds params specs monos));
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
+ Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
(ind_decl false);
val _ =
- Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
+ Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
(ind_decl true);
val _ =
--- a/src/HOL/Tools/inductive_set.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Sep 12 15:01:25 2012 +0200
@@ -21,7 +21,7 @@
(binding * string option * mixfix) list ->
(binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
- bool -> local_theory -> Inductive.inductive_result * local_theory
+ local_theory -> Inductive.inductive_result * local_theory
val mono_add: attribute
val mono_del: attribute
val codegen_preproc: theory -> thm list -> thm list
@@ -574,11 +574,11 @@
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
val _ =
- Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
+ Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
(ind_set_decl false);
val _ =
- Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
+ Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
(ind_set_decl true);
end;
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Sep 12 15:01:25 2012 +0200
@@ -57,7 +57,7 @@
val dest_sum = Arith_Data.dest_sum;
val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
-val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT;
+val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} dummyT;
val mk_times = HOLogic.mk_binop @{const_name Groups.times};
@@ -79,7 +79,7 @@
fun long_mk_prod T [] = one_of T
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
-val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name Groups.times} dummyT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -262,7 +262,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
val bal_add1 = @{thm eq_add_iff1} RS trans
val bal_add2 = @{thm eq_add_iff2} RS trans
);
@@ -270,7 +270,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
val bal_add1 = @{thm less_add_iff1} RS trans
val bal_add2 = @{thm less_add_iff2} RS trans
);
@@ -278,7 +278,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
val bal_add1 = @{thm le_add_iff1} RS trans
val bal_add2 = @{thm le_add_iff2} RS trans
);
@@ -385,7 +385,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
val cancel = @{thm div_mult_mult1} RS trans
val neg_exchanges = false
)
@@ -394,7 +394,7 @@
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val mk_bal = HOLogic.mk_binop @{const_name Fields.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -402,7 +402,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
val cancel = @{thm mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -410,7 +410,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -418,7 +418,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -501,7 +501,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
@@ -509,7 +509,7 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
val simp_conv = sign_conv
@{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
);
@@ -518,7 +518,7 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
val simp_conv = sign_conv
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
);
@@ -527,14 +527,14 @@
structure DivCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
);
structure ModCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} dummyT
fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
);
@@ -542,7 +542,7 @@
structure DvdCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd}
- val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} dummyT
fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
);
@@ -550,7 +550,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val mk_bal = HOLogic.mk_binop @{const_name Fields.divide}
- val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
--- a/src/Pure/Concurrent/par_list.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Pure/Concurrent/par_list.ML Wed Sep 12 15:01:25 2012 +0200
@@ -33,14 +33,17 @@
not (Multithreading.enabled ()) orelse Multithreading.self_critical ()
then map (Exn.capture f) xs
else
- let
- val group = Future.new_group (Future.worker_group ());
- val futures =
- Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
- (map (fn x => fn () => f x) xs);
- val results = Future.join_results futures
- handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
- in results end;
+ uninterruptible (fn restore_attributes => fn () =>
+ let
+ val group = Future.new_group (Future.worker_group ());
+ val futures =
+ Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
+ (map (fn x => fn () => f x) xs);
+ val results =
+ restore_attributes Future.join_results futures
+ handle exn =>
+ (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+ in results end) ();
fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
fun map f = map_name "Par_List.map" f;
--- a/src/Pure/PIDE/isabelle_markup.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Wed Sep 12 15:01:25 2012 +0200
@@ -64,8 +64,8 @@
val doc_sourceN: string val doc_source: Markup.T
val antiqN: string val antiq: Markup.T
val ML_antiquotationN: string
- val doc_antiquotationN: string
- val doc_antiquotation_optionN: string
+ val document_antiquotationN: string
+ val document_antiquotation_optionN: string
val keywordN: string val keyword: Markup.T
val operatorN: string val operator: Markup.T
val commandN: string val command: Markup.T
@@ -169,7 +169,7 @@
val theoryN = "theory";
val classN = "class";
-val type_nameN = "type name";
+val type_nameN = "type_name";
val constantN = "constant";
val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
@@ -222,9 +222,9 @@
val (doc_sourceN, doc_source) = markup_elem "doc_source";
val (antiqN, antiq) = markup_elem "antiq";
-val ML_antiquotationN = "ML antiquotation";
-val doc_antiquotationN = "document antiquotation";
-val doc_antiquotation_optionN = "document antiquotation option";
+val ML_antiquotationN = "ML_antiquotation";
+val document_antiquotationN = "document_antiquotation";
+val document_antiquotation_optionN = "document_antiquotation_option";
(* outer syntax *)
--- a/src/Pure/PIDE/isabelle_markup.scala Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Wed Sep 12 15:01:25 2012 +0200
@@ -78,7 +78,7 @@
/* logical entities */
val CLASS = "class"
- val TYPE_NAME = "type name"
+ val TYPE_NAME = "type_name"
val FIXED = "fixed"
val CONSTANT = "constant"
@@ -115,12 +115,12 @@
/* embedded source text */
val ML_SOURCE = "ML_source"
- val DOC_SOURCE = "doc_source"
+ val DOCUMENT_SOURCE = "document_source"
val ANTIQ = "antiq"
- val ML_ANTIQUOTATION = "ML antiquotation"
- val DOCUMENT_ANTIQUOTATION = "document antiquotation"
- val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
+ val ML_ANTIQUOTATION = "ML_antiquotation"
+ val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
+ val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
/* ML syntax */
--- a/src/Pure/System/color_value.scala Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Pure/System/color_value.scala Wed Sep 12 15:01:25 2012 +0200
@@ -1,4 +1,4 @@
-/* Title: Pure/General/color_value.scala
+/* Title: Pure/System/color_value.scala
Module: PIDE
Author: Makarius
--- a/src/Pure/Thy/latex.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Pure/Thy/latex.ML Wed Sep 12 15:01:25 2012 +0200
@@ -30,22 +30,6 @@
structure Latex: LATEX =
struct
-(* literal text *)
-
-local
- fun hex_nibble i =
- if i < 10 then string_of_int i
- else chr (ord "A" + i - 10);
-
- fun hex_byte c = hex_nibble (ord c div 16) ^ hex_nibble (ord c mod 16);
-in
-
-fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
-fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
-
-end;
-
-
(* symbol output *)
local
@@ -90,7 +74,7 @@
| output_chr "\n" = "\\isanewline\n"
| output_chr c =
(case Symtab.lookup char_table c of
- SOME s => enclose_literal c s
+ SOME s => s
| NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
val output_chrs = translate_string output_chr;
@@ -99,12 +83,8 @@
(case Symbol.decode sym of
Symbol.Char s => output_chr s
| Symbol.UTF8 s => s
- | Symbol.Sym s =>
- if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
- else output_chrs sym
- | Symbol.Ctrl s =>
- if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
- else output_chrs sym
+ | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
+ | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
| Symbol.Raw s => s
| Symbol.Malformed s => error (Symbol.malformed_msg s)
| Symbol.EOF => error "Bad EOF symbol");
@@ -120,8 +100,8 @@
| Antiquote.Antiq (ss, _) =>
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
(output_symbols (map Symbol_Pos.symbol ss))
- | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
- | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
+ | Antiquote.Open _ => "{\\isaantiqopen}"
+ | Antiquote.Close _ => "{\\isaantiqclose}");
end;
@@ -138,23 +118,15 @@
else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
- output_syms s |> enclose
- (enclose_literal "\"" "{\\isachardoublequoteopen}")
- (enclose_literal "\"" "{\\isachardoublequoteclose}")
+ enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
else if Token.is_kind Token.AltString tok then
- output_syms s |> enclose
- (enclose_literal "`" "{\\isacharbackquoteopen}")
- (enclose_literal "`" "{\\isacharbackquoteclose}")
+ enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
val (txt, pos) = Token.source_position_of tok;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
- in
- out |> enclose
- (enclose_literal "{*" "{\\isacharverbatimopen}")
- (enclose_literal "*}" "{\\isacharverbatimclose}")
- end
+ in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else output_syms s
end;
--- a/src/Pure/Thy/thy_output.ML Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML Wed Sep 12 15:01:25 2012 +0200
@@ -83,8 +83,8 @@
(Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
- (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
- Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
+ (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
+ Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
val extend = I;
fun merge ((commands1, options1), (commands2, options2)) : T =
(Name_Space.merge_tables (commands1, commands2),
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 12 15:01:25 2012 +0200
@@ -70,7 +70,7 @@
Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
- Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
+ Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
{
@@ -163,7 +163,7 @@
Isabelle_Markup.TFREE -> "free type variable",
Isabelle_Markup.TVAR -> "schematic type variable",
Isabelle_Markup.ML_SOURCE -> "ML source",
- Isabelle_Markup.DOC_SOURCE -> "document source")
+ Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
private val tooltip_elements =
Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
@@ -183,7 +183,8 @@
range, Text.Info(range, Nil), Some(tooltip_elements),
{
case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
- add(prev, r, (true, kind + " " + quote(name)))
+ val kind1 = space_explode('_', kind).mkString(" ")
+ add(prev, r, (true, kind1 + " " + quote(name)))
case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
--- a/src/Tools/jEdit/src/jedit_options.scala Wed Sep 12 12:43:34 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Wed Sep 12 15:01:25 2012 +0200
@@ -68,7 +68,13 @@
name = opt_name
val title = opt_title
def load = text = value.check_name(opt_name).value
- def save = update(value + (opt_name, text))
+ def save =
+ try { update(value + (opt_name, text)) }
+ catch {
+ case ERROR(msg) =>
+ Library.error_dialog(this.peer, "Failed to update options",
+ Library.scrollable_text(msg))
+ }
}
text_area.peer.setInputVerifier(new InputVerifier {
def verify(jcomponent: JComponent): Boolean =