# HG changeset patch # User wenzelm # Date 1347454885 -7200 # Node ID 77c7ce7609cd866f48423c730ce6ce50f470320f # Parent f4169aa675130f4b53aa4fbfcf063c3afd78f8c1# Parent 4f28543ae7fab0da82484139e9e024fd5b8b71cb merged diff -r f4169aa67513 -r 77c7ce7609cd lib/texinputs/isabelle.sty --- 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{\%}}% diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/Functions/Functions.thy --- 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. diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/IsarRef/document/build --- 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" . diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/ROOT --- 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" diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/Tutorial/Protocol/Event.thy --- 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 diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/Tutorial/Protocol/Message.thy --- 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; diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/Tutorial/Protocol/NS_Public.thy --- 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. diff -r f4169aa67513 -r 77c7ce7609cd src/Doc/pdfsetup.sty --- 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 <>> BDC}#2\pdfliteral direct{EMC}} -\renewcommand{\isanil}{{\color{white}.}} -\fi diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/Library/Prefix_Order.thy --- 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 *) diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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 "\ x. \ y. \ (x \ y)"} | Nand => @{term "\ x. \ y. \ (x \ 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 => diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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) diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/Tools/inductive.ML --- 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 _ = diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/Tools/inductive_set.ML --- 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; diff -r f4169aa67513 -r 77c7ce7609cd src/HOL/Tools/numeral_simprocs.ML --- 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} ); diff -r f4169aa67513 -r 77c7ce7609cd src/Pure/Concurrent/par_list.ML --- 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; diff -r f4169aa67513 -r 77c7ce7609cd src/Pure/PIDE/isabelle_markup.ML --- 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 *) diff -r f4169aa67513 -r 77c7ce7609cd src/Pure/PIDE/isabelle_markup.scala --- 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 */ diff -r f4169aa67513 -r 77c7ce7609cd src/Pure/System/color_value.scala --- 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 diff -r f4169aa67513 -r 77c7ce7609cd src/Pure/Thy/latex.ML --- 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 "\\" "{\\isaantiqopen}" - | Antiquote.Close _ => enclose_literal "\\" "{\\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; diff -r f4169aa67513 -r 77c7ce7609cd src/Pure/Thy/thy_output.ML --- 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), diff -r f4169aa67513 -r 77c7ce7609cd src/Tools/jEdit/src/isabelle_rendering.scala --- 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)) diff -r f4169aa67513 -r 77c7ce7609cd src/Tools/jEdit/src/jedit_options.scala --- 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 =