merged
authorwenzelm
Wed Sep 12 15:01:25 2012 +0200 (2012-09-12)
changeset 4933277c7ce7609cd
parent 49331 f4169aa67513
parent 49324 4f28543ae7fa
child 49333 8b144338e1a2
merged
     1.1 --- a/lib/texinputs/isabelle.sty	Wed Sep 12 12:43:34 2012 +0200
     1.2 +++ b/lib/texinputs/isabelle.sty	Wed Sep 12 15:01:25 2012 +0200
     1.3 @@ -103,9 +103,6 @@
     1.4  \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
     1.5  }
     1.6  
     1.7 -\newcommand{\isaliteral}[2]{#2}
     1.8 -\newcommand{\isanil}{}
     1.9 -
    1.10  
    1.11  % keyword and section markup
    1.12  
    1.13 @@ -158,9 +155,9 @@
    1.14  \isachardefaults%
    1.15  \def\isacharunderscorekeyword{\mbox{-}}%
    1.16  \def\isacharbang{\isamath{!}}%
    1.17 -\def\isachardoublequote{\isanil}%
    1.18 -\def\isachardoublequoteopen{\isanil}%
    1.19 -\def\isachardoublequoteclose{\isanil}%
    1.20 +\def\isachardoublequote{}%
    1.21 +\def\isachardoublequoteopen{}%
    1.22 +\def\isachardoublequoteclose{}%
    1.23  \def\isacharhash{\isamath{\#}}%
    1.24  \def\isachardollar{\isamath{\$}}%
    1.25  \def\isacharpercent{\isamath{\%}}%
     2.1 --- a/src/Doc/Functions/Functions.thy	Wed Sep 12 12:43:34 2012 +0200
     2.2 +++ b/src/Doc/Functions/Functions.thy	Wed Sep 12 15:01:25 2012 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Doc/Functions/Thy/Fundefs.thy
     2.5 +(*  Title:      Doc/Functions/Fundefs.thy
     2.6      Author:     Alexander Krauss, TU Muenchen
     2.7  
     2.8  Tutorial for function definitions with the new "function" package.
     3.1 --- a/src/Doc/IsarRef/document/build	Wed Sep 12 12:43:34 2012 +0200
     3.2 +++ b/src/Doc/IsarRef/document/build	Wed Sep 12 15:01:25 2012 +0200
     3.3 @@ -11,7 +11,6 @@
     3.4  cp "$ISABELLE_HOME/src/Doc/extra.sty" .
     3.5  cp "$ISABELLE_HOME/src/Doc/isar.sty" .
     3.6  cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
     3.7 -cp "$ISABELLE_HOME/src/Doc/isar.sty" .
     3.8  cp "$ISABELLE_HOME/src/Doc/underscore.sty" .
     3.9  cp "$ISABELLE_HOME/src/Doc/manual.bib" .
    3.10  
     4.1 --- a/src/Doc/ROOT	Wed Sep 12 12:43:34 2012 +0200
     4.2 +++ b/src/Doc/ROOT	Wed Sep 12 15:01:25 2012 +0200
     4.3 @@ -5,6 +5,11 @@
     4.4    files
     4.5      "../prepare_document"
     4.6      "../pdfsetup.sty"
     4.7 +    "../iman.sty"
     4.8 +    "../extra.sty"
     4.9 +    "../isar.sty"
    4.10 +    "../proof.sty"
    4.11 +    "../manual.bib"
    4.12      "document/build"
    4.13      "document/root.tex"
    4.14      "document/style.sty"
    4.15 @@ -23,6 +28,11 @@
    4.16    files
    4.17      "../prepare_document"
    4.18      "../pdfsetup.sty"
    4.19 +    "../iman.sty"
    4.20 +    "../extra.sty"
    4.21 +    "../isar.sty"
    4.22 +    "../proof.sty"
    4.23 +    "../manual.bib"
    4.24      "document/adapt.tex"
    4.25      "document/architecture.tex"
    4.26      "document/build"
    4.27 @@ -80,8 +90,8 @@
    4.28      "../extra.sty"
    4.29      "../isar.sty"
    4.30      "../proof.sty"
    4.31 +    "../ttbox.sty"
    4.32      "../underscore.sty"
    4.33 -    "../ttbox.sty"
    4.34      "../manual.bib"
    4.35      "document/build"
    4.36      "document/root.tex"
    4.37 @@ -110,9 +120,9 @@
    4.38      "../pdfsetup.sty"
    4.39      "../iman.sty"
    4.40      "../extra.sty"
    4.41 +    "../isar.sty"
    4.42      "../ttbox.sty"
    4.43 -    "../proof.sty"
    4.44 -    "../isar.sty"
    4.45 +    "../underscore.sty"
    4.46      "../manual.bib"
    4.47      "document/build"
    4.48      "document/isar-vm.eps"
    4.49 @@ -285,8 +295,8 @@
    4.50      "../pdfsetup.sty"
    4.51      "../iman.sty"
    4.52      "../extra.sty"
    4.53 +    "../isar.sty"
    4.54      "../ttbox.sty"
    4.55 -    "../isar.sty"
    4.56      "../underscore.sty"
    4.57      "../manual.bib"
    4.58      "document/browser_screenshot.eps"
     5.1 --- a/src/Doc/Tutorial/Protocol/Event.thy	Wed Sep 12 12:43:34 2012 +0200
     5.2 +++ b/src/Doc/Tutorial/Protocol/Event.thy	Wed Sep 12 15:01:25 2012 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4 -(*  Title:      HOL/Auth/Event
     5.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.6 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7      Copyright   1996  University of Cambridge
     5.8  
     5.9  Datatype of events; function "spies"; freshness
     6.1 --- a/src/Doc/Tutorial/Protocol/Message.thy	Wed Sep 12 12:43:34 2012 +0200
     6.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy	Wed Sep 12 15:01:25 2012 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4 -(*  Title:      HOL/Auth/Message
     6.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.6 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7      Copyright   1996  University of Cambridge
     6.8  
     6.9  Datatypes of agents and messages;
     7.1 --- a/src/Doc/Tutorial/Protocol/NS_Public.thy	Wed Sep 12 12:43:34 2012 +0200
     7.2 +++ b/src/Doc/Tutorial/Protocol/NS_Public.thy	Wed Sep 12 15:01:25 2012 +0200
     7.3 @@ -1,5 +1,4 @@
     7.4 -(*  Title:      HOL/Auth/NS_Public
     7.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7      Copyright   1996  University of Cambridge
     7.8  
     7.9  Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     8.1 --- a/src/Doc/pdfsetup.sty	Wed Sep 12 12:43:34 2012 +0200
     8.2 +++ b/src/Doc/pdfsetup.sty	Wed Sep 12 15:01:25 2012 +0200
     8.3 @@ -15,13 +15,3 @@
     8.4  \urlstyle{rm}
     8.5  \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
     8.6  
     8.7 -\def\isaliteral#1#2{#2}
     8.8 -\def\isanil{}
     8.9 -
    8.10 -%experimental treatment of replacement text
    8.11 -\iffalse
    8.12 -\ifnum\pdfminorversion<5\pdfminorversion=5\fi
    8.13 -\renewcommand{\isaliteral}[2]{%
    8.14 -\pdfliteral direct{/Span <</ActualText<#1>>> BDC}#2\pdfliteral direct{EMC}}
    8.15 -\renewcommand{\isanil}{{\color{white}.}}
    8.16 -\fi
     9.1 --- a/src/HOL/Library/Prefix_Order.thy	Wed Sep 12 12:43:34 2012 +0200
     9.2 +++ b/src/HOL/Library/Prefix_Order.thy	Wed Sep 12 15:01:25 2012 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Library/Sublist.thy
     9.5 +(*  Title:      HOL/Library/Prefix_Order.thy
     9.6      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     9.7  *)
     9.8  
    10.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Sep 12 12:43:34 2012 +0200
    10.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Sep 12 15:01:25 2012 +0200
    10.3 @@ -316,8 +316,8 @@
    10.4      fun body 0 t = t
    10.5        | body n t = body (n - 1) (t  $ (Bound (n - 1)))
    10.6    in
    10.7 -    body n (Const (str, Term.dummyT))
    10.8 -    |> funpow n (Term.absdummy Term.dummyT)
    10.9 +    body n (Const (str, dummyT))
   10.10 +    |> funpow n (Term.absdummy dummyT)
   10.11    end
   10.12  fun mk_fun_type [] b acc = acc b
   10.13    | mk_fun_type (ty :: tys) b acc =
   10.14 @@ -365,10 +365,10 @@
   10.15            (string_of_interpreted_symbol interpreted_symbol))), [])
   10.16     | Interpreted_Logic logic_symbol =>
   10.17         (case logic_symbol of
   10.18 -          Equals => HOLogic.eq_const Term.dummyT
   10.19 +          Equals => HOLogic.eq_const dummyT
   10.20          | NEquals =>
   10.21 -           HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0)
   10.22 -           |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
   10.23 +           HOLogic.mk_not (HOLogic.eq_const dummyT $ Bound 1 $ Bound 0)
   10.24 +           |> (Term.absdummy dummyT #> Term.absdummy dummyT)
   10.25          | Or => HOLogic.disj
   10.26          | And => HOLogic.conj
   10.27          | Iff => HOLogic.eq_const HOLogic.boolT
   10.28 @@ -380,8 +380,8 @@
   10.29          | Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}
   10.30          | Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}
   10.31          | Not => HOLogic.Not
   10.32 -        | Op_Forall => HOLogic.all_const Term.dummyT
   10.33 -        | Op_Exists => HOLogic.exists_const Term.dummyT
   10.34 +        | Op_Forall => HOLogic.all_const dummyT
   10.35 +        | Op_Exists => HOLogic.exists_const dummyT
   10.36          | True => @{term "True"}
   10.37          | False => @{term "False"}
   10.38          )
   10.39 @@ -404,7 +404,7 @@
   10.40  fun mtimes thy =
   10.41    fold (fn x => fn y =>
   10.42      Sign.mk_const thy
   10.43 -    ("Product_Type.Pair", [Term.dummyT, Term.dummyT]) $ y $ x)
   10.44 +    ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
   10.45  
   10.46  fun mtimes' (args, thy) f =
   10.47    let
   10.48 @@ -530,7 +530,7 @@
   10.49             SOME ty =>
   10.50               (case ty of
   10.51                  SOME ty => Free (n, ty)
   10.52 -              | NONE => Free (n, Term.dummyT) (*to infer the variable's type*)
   10.53 +              | NONE => Free (n, dummyT) (*to infer the variable's type*)
   10.54               )
   10.55           | NONE =>
   10.56               raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
   10.57 @@ -621,7 +621,7 @@
   10.58                   case ty of
   10.59                     NONE =>
   10.60                       f (n,
   10.61 -                        if language = THF then Term.dummyT
   10.62 +                        if language = THF then dummyT
   10.63                          else
   10.64                            interpret_type config thy type_map
   10.65                             (Defined_type Type_Ind),
   10.66 @@ -646,12 +646,12 @@
   10.67              let val (t, thy') =
   10.68                interpret_formula config language const_map var_types type_map
   10.69                 (Quant (Lambda, bindings, tptp_formula)) thy
   10.70 -            in ((HOLogic.choice_const Term.dummyT) $ t, thy') end
   10.71 +            in ((HOLogic.choice_const dummyT) $ t, thy') end
   10.72          | Iota =>
   10.73              let val (t, thy') =
   10.74                interpret_formula config language const_map var_types type_map
   10.75                 (Quant (Lambda, bindings, tptp_formula)) thy
   10.76 -            in (Const (@{const_name The}, Term.dummyT) $ t, thy') end
   10.77 +            in (Const (@{const_name The}, dummyT) $ t, thy') end
   10.78          | Dep_Prod =>
   10.79              raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
   10.80          | Dep_Sum =>
    11.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Sep 12 12:43:34 2012 +0200
    11.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Sep 12 15:01:25 2012 +0200
    11.3 @@ -380,7 +380,7 @@
    11.4  
    11.5  (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
    11.6  local
    11.7 -  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
    11.8 +  val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
    11.9    fun default c = const_prefix ^ lookup_const c
   11.10  in
   11.11    fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 12 12:43:34 2012 +0200
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 12 15:01:25 2012 +0200
    12.3 @@ -38,7 +38,7 @@
    12.4    end
    12.5  
    12.6  fun pred_of_function thy name =
    12.7 -  case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
    12.8 +  case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
    12.9      [] => NONE
   12.10    | [(f, p)] => SOME (fst (dest_Const p))
   12.11    | _ => error ("Multiple matches possible for lookup of constant " ^ name)
    13.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 12 12:43:34 2012 +0200
    13.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 12 15:01:25 2012 +0200
    13.3 @@ -49,7 +49,7 @@
    13.4      (binding * string option * mixfix) list ->
    13.5      (Attrib.binding * string) list ->
    13.6      (Facts.ref * Attrib.src list) list ->
    13.7 -    bool -> local_theory -> inductive_result * local_theory
    13.8 +    local_theory -> inductive_result * local_theory
    13.9    val add_inductive_global: inductive_flags ->
   13.10      ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   13.11      thm list -> theory -> inductive_result * theory
   13.12 @@ -81,8 +81,8 @@
   13.13      (binding * string option * mixfix) list ->
   13.14      (binding * string option * mixfix) list ->
   13.15      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
   13.16 -    bool -> local_theory -> inductive_result * local_theory
   13.17 -  val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
   13.18 +    local_theory -> inductive_result * local_theory
   13.19 +  val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
   13.20  end;
   13.21  
   13.22  structure Inductive: INDUCTIVE =
   13.23 @@ -1039,7 +1039,7 @@
   13.24      ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
   13.25    end;
   13.26  
   13.27 -fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
   13.28 +fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
   13.29    let
   13.30      val ((vars, intrs), _) = lthy
   13.31        |> Proof_Context.set_mode Proof_Context.mode_abbrev
   13.32 @@ -1143,16 +1143,16 @@
   13.33    Scan.optional Parse_Spec.where_alt_specs [] --
   13.34    Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
   13.35    >> (fn (((preds, params), specs), monos) =>
   13.36 -      (snd oo gen_add_inductive mk_def true coind preds params specs monos));
   13.37 +      (snd o gen_add_inductive mk_def true coind preds params specs monos));
   13.38  
   13.39  val ind_decl = gen_ind_decl add_ind_def;
   13.40  
   13.41  val _ =
   13.42 -  Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
   13.43 +  Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
   13.44      (ind_decl false);
   13.45  
   13.46  val _ =
   13.47 -  Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
   13.48 +  Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
   13.49      (ind_decl true);
   13.50  
   13.51  val _ =
    14.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Sep 12 12:43:34 2012 +0200
    14.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 12 15:01:25 2012 +0200
    14.3 @@ -21,7 +21,7 @@
    14.4      (binding * string option * mixfix) list ->
    14.5      (binding * string option * mixfix) list ->
    14.6      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
    14.7 -    bool -> local_theory -> Inductive.inductive_result * local_theory
    14.8 +    local_theory -> Inductive.inductive_result * local_theory
    14.9    val mono_add: attribute
   14.10    val mono_del: attribute
   14.11    val codegen_preproc: theory -> thm list -> thm list
   14.12 @@ -574,11 +574,11 @@
   14.13  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
   14.14  
   14.15  val _ =
   14.16 -  Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
   14.17 +  Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
   14.18      (ind_set_decl false);
   14.19  
   14.20  val _ =
   14.21 -  Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
   14.22 +  Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
   14.23      (ind_set_decl true);
   14.24  
   14.25  end;
    15.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Sep 12 12:43:34 2012 +0200
    15.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Sep 12 15:01:25 2012 +0200
    15.3 @@ -57,7 +57,7 @@
    15.4  val dest_sum = Arith_Data.dest_sum;
    15.5  
    15.6  val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
    15.7 -val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT;
    15.8 +val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} dummyT;
    15.9  
   15.10  val mk_times = HOLogic.mk_binop @{const_name Groups.times};
   15.11  
   15.12 @@ -79,7 +79,7 @@
   15.13  fun long_mk_prod T []        = one_of T
   15.14    | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
   15.15  
   15.16 -val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT;
   15.17 +val dest_times = HOLogic.dest_bin @{const_name Groups.times} dummyT;
   15.18  
   15.19  fun dest_prod t =
   15.20        let val (t,u) = dest_times t
   15.21 @@ -262,7 +262,7 @@
   15.22  structure EqCancelNumerals = CancelNumeralsFun
   15.23   (open CancelNumeralsCommon
   15.24    val mk_bal   = HOLogic.mk_eq
   15.25 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   15.26 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   15.27    val bal_add1 = @{thm eq_add_iff1} RS trans
   15.28    val bal_add2 = @{thm eq_add_iff2} RS trans
   15.29  );
   15.30 @@ -270,7 +270,7 @@
   15.31  structure LessCancelNumerals = CancelNumeralsFun
   15.32   (open CancelNumeralsCommon
   15.33    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   15.34 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   15.35 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   15.36    val bal_add1 = @{thm less_add_iff1} RS trans
   15.37    val bal_add2 = @{thm less_add_iff2} RS trans
   15.38  );
   15.39 @@ -278,7 +278,7 @@
   15.40  structure LeCancelNumerals = CancelNumeralsFun
   15.41   (open CancelNumeralsCommon
   15.42    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   15.43 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   15.44 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   15.45    val bal_add1 = @{thm le_add_iff1} RS trans
   15.46    val bal_add2 = @{thm le_add_iff2} RS trans
   15.47  );
   15.48 @@ -385,7 +385,7 @@
   15.49  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   15.50   (open CancelNumeralFactorCommon
   15.51    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   15.52 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
   15.53 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
   15.54    val cancel = @{thm div_mult_mult1} RS trans
   15.55    val neg_exchanges = false
   15.56  )
   15.57 @@ -394,7 +394,7 @@
   15.58  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   15.59   (open CancelNumeralFactorCommon
   15.60    val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
   15.61 -  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
   15.62 +  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
   15.63    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   15.64    val neg_exchanges = false
   15.65  )
   15.66 @@ -402,7 +402,7 @@
   15.67  structure EqCancelNumeralFactor = CancelNumeralFactorFun
   15.68   (open CancelNumeralFactorCommon
   15.69    val mk_bal   = HOLogic.mk_eq
   15.70 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   15.71 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   15.72    val cancel = @{thm mult_cancel_left} RS trans
   15.73    val neg_exchanges = false
   15.74  )
   15.75 @@ -410,7 +410,7 @@
   15.76  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   15.77   (open CancelNumeralFactorCommon
   15.78    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   15.79 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   15.80 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   15.81    val cancel = @{thm mult_less_cancel_left} RS trans
   15.82    val neg_exchanges = true
   15.83  )
   15.84 @@ -418,7 +418,7 @@
   15.85  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   15.86   (open CancelNumeralFactorCommon
   15.87    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   15.88 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   15.89 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   15.90    val cancel = @{thm mult_le_cancel_left} RS trans
   15.91    val neg_exchanges = true
   15.92  )
   15.93 @@ -501,7 +501,7 @@
   15.94  structure EqCancelFactor = ExtractCommonTermFun
   15.95   (open CancelFactorCommon
   15.96    val mk_bal   = HOLogic.mk_eq
   15.97 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
   15.98 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   15.99    fun simp_conv _ _ = SOME @{thm mult_cancel_left}
  15.100  );
  15.101  
  15.102 @@ -509,7 +509,7 @@
  15.103  structure LeCancelFactor = ExtractCommonTermFun
  15.104   (open CancelFactorCommon
  15.105    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
  15.106 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
  15.107 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
  15.108    val simp_conv = sign_conv
  15.109      @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
  15.110  );
  15.111 @@ -518,7 +518,7 @@
  15.112  structure LessCancelFactor = ExtractCommonTermFun
  15.113   (open CancelFactorCommon
  15.114    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
  15.115 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
  15.116 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
  15.117    val simp_conv = sign_conv
  15.118      @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
  15.119  );
  15.120 @@ -527,14 +527,14 @@
  15.121  structure DivCancelFactor = ExtractCommonTermFun
  15.122   (open CancelFactorCommon
  15.123    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
  15.124 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
  15.125 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
  15.126    fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
  15.127  );
  15.128  
  15.129  structure ModCancelFactor = ExtractCommonTermFun
  15.130   (open CancelFactorCommon
  15.131    val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
  15.132 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
  15.133 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} dummyT
  15.134    fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
  15.135  );
  15.136  
  15.137 @@ -542,7 +542,7 @@
  15.138  structure DvdCancelFactor = ExtractCommonTermFun
  15.139   (open CancelFactorCommon
  15.140    val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
  15.141 -  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT
  15.142 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} dummyT
  15.143    fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
  15.144  );
  15.145  
  15.146 @@ -550,7 +550,7 @@
  15.147  structure DivideCancelFactor = ExtractCommonTermFun
  15.148   (open CancelFactorCommon
  15.149    val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
  15.150 -  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
  15.151 +  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
  15.152    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
  15.153  );
  15.154  
    16.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Sep 12 12:43:34 2012 +0200
    16.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Sep 12 15:01:25 2012 +0200
    16.3 @@ -33,14 +33,17 @@
    16.4        not (Multithreading.enabled ()) orelse Multithreading.self_critical ()
    16.5    then map (Exn.capture f) xs
    16.6    else
    16.7 -    let
    16.8 -      val group = Future.new_group (Future.worker_group ());
    16.9 -      val futures =
   16.10 -        Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
   16.11 -          (map (fn x => fn () => f x) xs);
   16.12 -      val results = Future.join_results futures
   16.13 -        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
   16.14 -    in results end;
   16.15 +    uninterruptible (fn restore_attributes => fn () =>
   16.16 +      let
   16.17 +        val group = Future.new_group (Future.worker_group ());
   16.18 +        val futures =
   16.19 +          Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
   16.20 +            (map (fn x => fn () => f x) xs);
   16.21 +        val results =
   16.22 +          restore_attributes Future.join_results futures
   16.23 +            handle exn =>
   16.24 +              (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
   16.25 +      in results end) ();
   16.26  
   16.27  fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
   16.28  fun map f = map_name "Par_List.map" f;
    17.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Wed Sep 12 12:43:34 2012 +0200
    17.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Wed Sep 12 15:01:25 2012 +0200
    17.3 @@ -64,8 +64,8 @@
    17.4    val doc_sourceN: string val doc_source: Markup.T
    17.5    val antiqN: string val antiq: Markup.T
    17.6    val ML_antiquotationN: string
    17.7 -  val doc_antiquotationN: string
    17.8 -  val doc_antiquotation_optionN: string
    17.9 +  val document_antiquotationN: string
   17.10 +  val document_antiquotation_optionN: string
   17.11    val keywordN: string val keyword: Markup.T
   17.12    val operatorN: string val operator: Markup.T
   17.13    val commandN: string val command: Markup.T
   17.14 @@ -169,7 +169,7 @@
   17.15  
   17.16  val theoryN = "theory";
   17.17  val classN = "class";
   17.18 -val type_nameN = "type name";
   17.19 +val type_nameN = "type_name";
   17.20  val constantN = "constant";
   17.21  
   17.22  val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
   17.23 @@ -222,9 +222,9 @@
   17.24  val (doc_sourceN, doc_source) = markup_elem "doc_source";
   17.25  
   17.26  val (antiqN, antiq) = markup_elem "antiq";
   17.27 -val ML_antiquotationN = "ML antiquotation";
   17.28 -val doc_antiquotationN = "document antiquotation";
   17.29 -val doc_antiquotation_optionN = "document antiquotation option";
   17.30 +val ML_antiquotationN = "ML_antiquotation";
   17.31 +val document_antiquotationN = "document_antiquotation";
   17.32 +val document_antiquotation_optionN = "document_antiquotation_option";
   17.33  
   17.34  
   17.35  (* outer syntax *)
    18.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 12 12:43:34 2012 +0200
    18.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 12 15:01:25 2012 +0200
    18.3 @@ -78,7 +78,7 @@
    18.4    /* logical entities */
    18.5  
    18.6    val CLASS = "class"
    18.7 -  val TYPE_NAME = "type name"
    18.8 +  val TYPE_NAME = "type_name"
    18.9    val FIXED = "fixed"
   18.10    val CONSTANT = "constant"
   18.11  
   18.12 @@ -115,12 +115,12 @@
   18.13    /* embedded source text */
   18.14  
   18.15    val ML_SOURCE = "ML_source"
   18.16 -  val DOC_SOURCE = "doc_source"
   18.17 +  val DOCUMENT_SOURCE = "document_source"
   18.18  
   18.19    val ANTIQ = "antiq"
   18.20 -  val ML_ANTIQUOTATION = "ML antiquotation"
   18.21 -  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
   18.22 -  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
   18.23 +  val ML_ANTIQUOTATION = "ML_antiquotation"
   18.24 +  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   18.25 +  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
   18.26  
   18.27  
   18.28    /* ML syntax */
    19.1 --- a/src/Pure/System/color_value.scala	Wed Sep 12 12:43:34 2012 +0200
    19.2 +++ b/src/Pure/System/color_value.scala	Wed Sep 12 15:01:25 2012 +0200
    19.3 @@ -1,4 +1,4 @@
    19.4 -/*  Title:      Pure/General/color_value.scala
    19.5 +/*  Title:      Pure/System/color_value.scala
    19.6      Module:     PIDE
    19.7      Author:     Makarius
    19.8  
    20.1 --- a/src/Pure/Thy/latex.ML	Wed Sep 12 12:43:34 2012 +0200
    20.2 +++ b/src/Pure/Thy/latex.ML	Wed Sep 12 15:01:25 2012 +0200
    20.3 @@ -30,22 +30,6 @@
    20.4  structure Latex: LATEX =
    20.5  struct
    20.6  
    20.7 -(* literal text *)
    20.8 -
    20.9 -local
   20.10 -  fun hex_nibble i =
   20.11 -    if i < 10 then string_of_int i
   20.12 -    else chr (ord "A" + i - 10);
   20.13 -
   20.14 -  fun hex_byte c = hex_nibble (ord c div 16) ^ hex_nibble (ord c mod 16);
   20.15 -in
   20.16 -
   20.17 -fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
   20.18 -fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
   20.19 -
   20.20 -end;
   20.21 -
   20.22 -
   20.23  (* symbol output *)
   20.24  
   20.25  local
   20.26 @@ -90,7 +74,7 @@
   20.27    | output_chr "\n" = "\\isanewline\n"
   20.28    | output_chr c =
   20.29        (case Symtab.lookup char_table c of
   20.30 -        SOME s => enclose_literal c s
   20.31 +        SOME s => s
   20.32        | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
   20.33  
   20.34  val output_chrs = translate_string output_chr;
   20.35 @@ -99,12 +83,8 @@
   20.36    (case Symbol.decode sym of
   20.37      Symbol.Char s => output_chr s
   20.38    | Symbol.UTF8 s => s
   20.39 -  | Symbol.Sym s =>
   20.40 -      if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
   20.41 -      else output_chrs sym
   20.42 -  | Symbol.Ctrl s =>
   20.43 -      if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
   20.44 -      else output_chrs sym
   20.45 +  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
   20.46 +  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
   20.47    | Symbol.Raw s => s
   20.48    | Symbol.Malformed s => error (Symbol.malformed_msg s)
   20.49    | Symbol.EOF => error "Bad EOF symbol");
   20.50 @@ -120,8 +100,8 @@
   20.51      | Antiquote.Antiq (ss, _) =>
   20.52          enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
   20.53            (output_symbols (map Symbol_Pos.symbol ss))
   20.54 -    | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
   20.55 -    | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
   20.56 +    | Antiquote.Open _ => "{\\isaantiqopen}"
   20.57 +    | Antiquote.Close _ => "{\\isaantiqclose}");
   20.58  
   20.59  end;
   20.60  
   20.61 @@ -138,23 +118,15 @@
   20.62      else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
   20.63        "\\isakeyword{" ^ output_syms s ^ "}"
   20.64      else if Token.is_kind Token.String tok then
   20.65 -      output_syms s |> enclose
   20.66 -        (enclose_literal "\"" "{\\isachardoublequoteopen}")
   20.67 -        (enclose_literal "\"" "{\\isachardoublequoteclose}")
   20.68 +      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   20.69      else if Token.is_kind Token.AltString tok then
   20.70 -      output_syms s |> enclose
   20.71 -        (enclose_literal "`" "{\\isacharbackquoteopen}")
   20.72 -        (enclose_literal "`" "{\\isacharbackquoteclose}")
   20.73 +      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   20.74      else if Token.is_kind Token.Verbatim tok then
   20.75        let
   20.76          val (txt, pos) = Token.source_position_of tok;
   20.77          val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   20.78          val out = implode (map output_syms_antiq ants);
   20.79 -      in
   20.80 -        out |> enclose
   20.81 -          (enclose_literal "{*" "{\\isacharverbatimopen}")
   20.82 -          (enclose_literal "*}" "{\\isacharverbatimclose}")
   20.83 -      end
   20.84 +      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   20.85      else output_syms s
   20.86    end;
   20.87  
    21.1 --- a/src/Pure/Thy/thy_output.ML	Wed Sep 12 12:43:34 2012 +0200
    21.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Sep 12 15:01:25 2012 +0200
    21.3 @@ -83,8 +83,8 @@
    21.4      (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    21.5        (string -> Proof.context -> Proof.context) Name_Space.table;
    21.6    val empty : T =
    21.7 -    (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
    21.8 -      Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
    21.9 +    (Name_Space.empty_table Isabelle_Markup.document_antiquotationN,
   21.10 +      Name_Space.empty_table Isabelle_Markup.document_antiquotation_optionN);
   21.11    val extend = I;
   21.12    fun merge ((commands1, options1), (commands2, options2)) : T =
   21.13      (Name_Space.merge_tables (commands1, commands2),
    22.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 12:43:34 2012 +0200
    22.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 12 15:01:25 2012 +0200
    22.3 @@ -70,7 +70,7 @@
    22.4        Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
    22.5        Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
    22.6        Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
    22.7 -      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOC_SOURCE)
    22.8 +      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
    22.9  
   22.10    def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
   22.11    {
   22.12 @@ -163,7 +163,7 @@
   22.13        Isabelle_Markup.TFREE -> "free type variable",
   22.14        Isabelle_Markup.TVAR -> "schematic type variable",
   22.15        Isabelle_Markup.ML_SOURCE -> "ML source",
   22.16 -      Isabelle_Markup.DOC_SOURCE -> "document source")
   22.17 +      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
   22.18  
   22.19    private val tooltip_elements =
   22.20      Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
   22.21 @@ -183,7 +183,8 @@
   22.22          range, Text.Info(range, Nil), Some(tooltip_elements),
   22.23          {
   22.24            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
   22.25 -            add(prev, r, (true, kind + " " + quote(name)))
   22.26 +            val kind1 = space_explode('_', kind).mkString(" ")
   22.27 +            add(prev, r, (true, kind1 + " " + quote(name)))
   22.28            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
   22.29            if Path.is_ok(name) =>
   22.30              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    23.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Wed Sep 12 12:43:34 2012 +0200
    23.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Sep 12 15:01:25 2012 +0200
    23.3 @@ -68,7 +68,13 @@
    23.4              name = opt_name
    23.5              val title = opt_title
    23.6              def load = text = value.check_name(opt_name).value
    23.7 -            def save = update(value + (opt_name, text))
    23.8 +            def save =
    23.9 +              try { update(value + (opt_name, text)) }
   23.10 +              catch {
   23.11 +                case ERROR(msg) =>
   23.12 +                  Library.error_dialog(this.peer, "Failed to update options",
   23.13 +                    Library.scrollable_text(msg))
   23.14 +              }
   23.15            }
   23.16          text_area.peer.setInputVerifier(new InputVerifier {
   23.17            def verify(jcomponent: JComponent): Boolean =