Merge
authorpaulson <lp15@cam.ac.uk>
Tue Mar 17 14:16:16 2015 +0000 (2015-03-17)
changeset 59732f13bb49dba08
parent 59731 7fccaeec22f0
parent 59729 ba54b27d733d
child 59733 cd945dc13bec
Merge
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Mar 17 12:23:56 2015 +0000
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Mar 17 14:16:16 2015 +0000
     1.3 @@ -552,7 +552,8 @@
     1.4  \noindent
     1.5  The main constituents of a constructor specification are the name of the
     1.6  constructor and the list of its argument types. An optional discriminator name
     1.7 -can be supplied at the front to override the default, which is
     1.8 +can be supplied at the front. If discriminators are enabled (cf.\ the
     1.9 +@{text "discs_sels"} option) but no name is supplied, the default is
    1.10  @{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
    1.11  @{text t.is_C\<^sub>j} otherwise.
    1.12  
    1.13 @@ -566,9 +567,10 @@
    1.14  The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
    1.15  
    1.16  In addition to the type of a constructor argument, it is possible to specify a
    1.17 -name for the corresponding selector to override the default name
    1.18 -(@{text un_C\<^sub>ji}). The same selector names can be reused for several
    1.19 -constructors as long as they share the same type.
    1.20 +name for the corresponding selector. The same selector name can be reused for
    1.21 +arguments to several constructors as long as the arguments share the same type.
    1.22 +If selectors are enabled (cf.\ the @{text "discs_sels"} option) but no name is
    1.23 +supplied, the default name is @{text un_C\<^sub>ji}.
    1.24  *}
    1.25  
    1.26  
    1.27 @@ -614,9 +616,7 @@
    1.28  @{text compat_tree.rec}).
    1.29  
    1.30  \item All types through which recursion takes place must be new-style datatypes
    1.31 -or the function type. In principle, it should be possible to support old-style
    1.32 -datatypes as well, but this has not been implemented yet (and there is currently
    1.33 -no way to register old-style datatypes as new-style datatypes).
    1.34 +or the function type.
    1.35  \end{itemize}
    1.36  *}
    1.37  
    1.38 @@ -625,7 +625,7 @@
    1.39    \label{ssec:datatype-generated-constants} *}
    1.40  
    1.41  text {*
    1.42 -Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m > 0$ live type variables
    1.43 +Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ live type variables
    1.44  and $n$ constructors @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the following
    1.45  auxiliary constants are introduced:
    1.46  
    1.47 @@ -653,6 +653,10 @@
    1.48  \medskip
    1.49  
    1.50  \noindent
    1.51 +The discriminators and selectors are generated only if the @{text "discs_sels"}
    1.52 +option is enabled or if names are specified for discriminators or selectors.
    1.53 +The set functions, map function, and relator are generated only if $m > 0$.
    1.54 +
    1.55  In addition, some of the plugins introduce their own constants
    1.56  (Section~\ref{sec:selecting-plugins}). The case combinator, discriminators,
    1.57  and selectors are collectively called \emph{destructors}. The prefix
    1.58 @@ -997,6 +1001,9 @@
    1.59  @{thm list.rel_map(1)[no_vars]} \\
    1.60  @{thm list.rel_map(2)[no_vars]}
    1.61  
    1.62 +\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
    1.63 +@{thm list.rel_refl[no_vars]}
    1.64 +
    1.65  \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\
    1.66  @{thm list.rel_mono[no_vars]} \\
    1.67  The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin
    1.68 @@ -3115,9 +3122,9 @@
    1.69    \label{ssec:lifting} *}
    1.70  
    1.71  text {*
    1.72 -For each (co)datatype with live type arguments and each manually registered BNF,
    1.73 -the \hthm{lifting} plugin generates properties and attributes that guide the
    1.74 -Lifting tool.
    1.75 +For each (co)datatype and each manually registered BNF with at least one live
    1.76 +type argument and no dead type arguments, the \hthm{lifting} plugin generates
    1.77 +properties and attributes that guide the Lifting tool.
    1.78  
    1.79  The plugin derives the following property:
    1.80  
    1.81 @@ -3226,8 +3233,8 @@
    1.82  Kun\v{c}ar implemented the @{text transfer} and @{text lifting} plugins.
    1.83  Florian Haftmann and Christian Urban provided general advice on Isabelle and
    1.84  package writing. Stefan Milius and Lutz Schr\"oder found an elegant proof that
    1.85 -eliminated one of the BNF proof obligations. Andreas Lochbihler and Christian
    1.86 -Sternagel suggested many textual improvements to this tutorial.
    1.87 +eliminated one of the BNF proof obligations. Andreas Lochbihler, Tobias Nipkow,
    1.88 +and Christian Sternagel suggested many textual improvements to this tutorial.
    1.89  *}
    1.90  
    1.91  end
     2.1 --- a/src/Doc/Logics_ZF/If.thy	Tue Mar 17 12:23:56 2015 +0000
     2.2 +++ b/src/Doc/Logics_ZF/If.thy	Tue Mar 17 14:16:16 2015 +0000
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Doc/ZF/If.thy
     2.5 +(*  Title:      Doc/Logics_ZF/If.thy
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   1991  University of Cambridge
     2.8  
     3.1 --- a/src/HOL/BNF_Def.thy	Tue Mar 17 12:23:56 2015 +0000
     3.2 +++ b/src/HOL/BNF_Def.thy	Tue Mar 17 14:16:16 2015 +0000
     3.3 @@ -228,6 +228,12 @@
     3.4  lemma comp_apply_eq: "f (g x) = h (k x) \<Longrightarrow> (f \<circ> g) x = (h \<circ> k) x"
     3.5    unfolding comp_apply by assumption
     3.6  
     3.7 +lemma refl_ge_eq: "(\<And>x. R x x) \<Longrightarrow> op = \<le> R"
     3.8 +  by auto
     3.9 +
    3.10 +lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x"
    3.11 +  by auto
    3.12 +
    3.13  ML_file "Tools/BNF/bnf_util.ML"
    3.14  ML_file "Tools/BNF/bnf_tactics.ML"
    3.15  ML_file "Tools/BNF/bnf_def_tactics.ML"
     4.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Tue Mar 17 12:23:56 2015 +0000
     4.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Tue Mar 17 14:16:16 2015 +0000
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      Code_Test_GHC.thy
     4.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_GHC.thy
     4.6      Author:     Andreas Lochbihler, ETH Zurich
     4.7  
     4.8  Test case for test_code on GHC
     5.1 --- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Tue Mar 17 12:23:56 2015 +0000
     5.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Tue Mar 17 14:16:16 2015 +0000
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      Code_Test_MLtonL.thy
     5.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_MLton.thy
     5.6      Author:     Andreas Lochbihler, ETH Zurich
     5.7  
     5.8  Test case for test_code on MLton
     6.1 --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Tue Mar 17 12:23:56 2015 +0000
     6.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Tue Mar 17 14:16:16 2015 +0000
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      Code_Test_OCaml.thy
     6.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_OCaml.thy
     6.6      Author:     Andreas Lochbihler, ETH Zurich
     6.7  
     6.8  Test case for test_code on OCaml
     7.1 --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Tue Mar 17 12:23:56 2015 +0000
     7.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Tue Mar 17 14:16:16 2015 +0000
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      Code_Test_PolyML.thy
     7.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
     7.6      Author:     Andreas Lochbihler, ETH Zurich
     7.7  
     7.8  Test case for test_code on PolyML
     8.1 --- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Tue Mar 17 12:23:56 2015 +0000
     8.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Tue Mar 17 14:16:16 2015 +0000
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      Code_Test_SMLNJ.thy
     8.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
     8.6      Author:     Andreas Lochbihler, ETH Zurich
     8.7  
     8.8  Test case for test_code on SMLNJ
     9.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Tue Mar 17 12:23:56 2015 +0000
     9.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Tue Mar 17 14:16:16 2015 +0000
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      Code_Test_Scala.thy
     9.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     9.6      Author:     Andreas Lochbihler, ETH Zurich
     9.7  
     9.8  Test case for test_code on Scala
    10.1 --- a/src/HOL/Groups_List.thy	Tue Mar 17 12:23:56 2015 +0000
    10.2 +++ b/src/HOL/Groups_List.thy	Tue Mar 17 14:16:16 2015 +0000
    10.3 @@ -237,6 +237,38 @@
    10.4    "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
    10.5    using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
    10.6  
    10.7 +lemma listsum_map_eq_setsum_count:
    10.8 +  "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) (set xs)"
    10.9 +proof(induction xs)
   10.10 +  case (Cons x xs)
   10.11 +  show ?case (is "?l = ?r")
   10.12 +  proof cases
   10.13 +    assume "x \<in> set xs"
   10.14 +    have "?l = f x + (\<Sum>x\<in>set xs. List.count xs x * f x)" by (simp add: Cons.IH)
   10.15 +    also have "set xs = insert x (set xs - {x})" using `x \<in> set xs`by blast
   10.16 +    also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). List.count xs x * f x) = ?r"
   10.17 +      by (simp add: setsum.insert_remove eq_commute)
   10.18 +    finally show ?thesis .
   10.19 +  next
   10.20 +    assume "x \<notin> set xs"
   10.21 +    hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast
   10.22 +    thus ?thesis by (simp add: Cons.IH `x \<notin> set xs`)
   10.23 +  qed
   10.24 +qed simp
   10.25 +
   10.26 +lemma listsum_map_eq_setsum_count2:
   10.27 +assumes "set xs \<subseteq> X" "finite X"
   10.28 +shows "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) X"
   10.29 +proof-
   10.30 +  let ?F = "\<lambda>x. List.count xs x * f x"
   10.31 +  have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
   10.32 +    using Un_absorb1[OF assms(1)] by(simp)
   10.33 +  also have "\<dots> = setsum ?F (set xs)"
   10.34 +    using assms(2)
   10.35 +    by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
   10.36 +  finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
   10.37 +qed
   10.38 +
   10.39  
   10.40  subsection {* Further facts about @{const List.n_lists} *}
   10.41  
    11.1 --- a/src/HOL/Inequalities.thy	Tue Mar 17 12:23:56 2015 +0000
    11.2 +++ b/src/HOL/Inequalities.thy	Tue Mar 17 14:16:16 2015 +0000
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:     Inequalities
    11.5 +(*  Title:     HOL/Inequalities.thy
    11.6      Author:    Tobias Nipkow
    11.7      Author:    Johannes Hölzl
    11.8  *)
    12.1 --- a/src/HOL/Library/Code_Test.thy	Tue Mar 17 12:23:56 2015 +0000
    12.2 +++ b/src/HOL/Library/Code_Test.thy	Tue Mar 17 14:16:16 2015 +0000
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      Code_Test.thy
    12.5 +(*  Title:      HOL/Library/Code_Test.thy
    12.6      Author:     Andreas Lochbihler, ETH Zurich
    12.7  
    12.8  Test infrastructure for the code generator
    13.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Mar 17 12:23:56 2015 +0000
    13.2 +++ b/src/HOL/Library/ContNotDenum.thy	Tue Mar 17 14:16:16 2015 +0000
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/Library/ContNonDenum.thy
    13.5 +(*  Title:      HOL/Library/ContNotDenum.thy
    13.6      Author:     Benjamin Porter, Monash University, NICTA, 2005
    13.7      Author:     Johannes Hölzl, TU München
    13.8  *)
    14.1 --- a/src/HOL/Library/code_test.ML	Tue Mar 17 12:23:56 2015 +0000
    14.2 +++ b/src/HOL/Library/code_test.ML	Tue Mar 17 14:16:16 2015 +0000
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      Code_Test.ML
    14.5 +(*  Title:      HOL/Library/code_test.ML
    14.6      Author:     Andreas Lochbihler, ETH Zurich
    14.7  
    14.8  Test infrastructure for the code generator
    15.1 --- a/src/HOL/Lifting.thy	Tue Mar 17 12:23:56 2015 +0000
    15.2 +++ b/src/HOL/Lifting.thy	Tue Mar 17 14:16:16 2015 +0000
    15.3 @@ -376,9 +376,6 @@
    15.4  lemma reflp_ge_eq:
    15.5    "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
    15.6  
    15.7 -lemma ge_eq_refl:
    15.8 -  "R \<ge> op= \<Longrightarrow> R x x" by blast
    15.9 -
   15.10  text {* Proving a parametrized correspondence relation *}
   15.11  
   15.12  definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
    16.1 --- a/src/HOL/List.thy	Tue Mar 17 12:23:56 2015 +0000
    16.2 +++ b/src/HOL/List.thy	Tue Mar 17 14:16:16 2015 +0000
    16.3 @@ -183,6 +183,12 @@
    16.4  
    16.5  hide_const (open) find
    16.6  
    16.7 +primrec count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
    16.8 +"count [] y = 0" |
    16.9 +"count (x#xs) y = (if x=y then count xs y + 1 else count xs y)"
   16.10 +
   16.11 +hide_const (open) count
   16.12 +
   16.13  definition
   16.14     "extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
   16.15  where "extract P xs =
   16.16 @@ -298,6 +304,7 @@
   16.17  @{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\
   16.18  @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
   16.19  @{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
   16.20 +@{lemma "List.count [0,1,0,2::int] 0 = 2" by (simp)}\\
   16.21  @{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
   16.22  @{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
   16.23  @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   16.24 @@ -2151,6 +2158,12 @@
   16.25    ultimately show ?thesis by auto
   16.26  qed
   16.27    
   16.28 +lemma take_update_cancel[simp]: "n \<le> m \<Longrightarrow> take n (xs[m := y]) = take n xs"
   16.29 +by(simp add: list_eq_iff_nth_eq)
   16.30 +
   16.31 +lemma drop_update_cancel[simp]: "n < m \<Longrightarrow> drop m (xs[n := x]) = drop m xs"
   16.32 +by(simp add: list_eq_iff_nth_eq)
   16.33 +
   16.34  lemma upd_conv_take_nth_drop:
   16.35    "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
   16.36  proof -
   16.37 @@ -2162,6 +2175,22 @@
   16.38    finally show ?thesis .
   16.39  qed
   16.40  
   16.41 +lemma take_update_swap: "n < m \<Longrightarrow> take m (xs[n := x]) = (take m xs)[n := x]"
   16.42 +apply(cases "n \<ge> length xs")
   16.43 + apply simp
   16.44 +apply(simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc
   16.45 +  split: nat.split)
   16.46 +done
   16.47 +
   16.48 +lemma drop_update_swap: "m \<le> n \<Longrightarrow> drop m (xs[n := x]) = (drop m xs)[n-m := x]"
   16.49 +apply(cases "n \<ge> length xs")
   16.50 + apply simp
   16.51 +apply(simp add: upd_conv_take_nth_drop drop_take)
   16.52 +done
   16.53 +
   16.54 +lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
   16.55 +by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
   16.56 +
   16.57  
   16.58  subsubsection {* @{const takeWhile} and @{const dropWhile} *}
   16.59  
   16.60 @@ -3211,6 +3240,9 @@
   16.61    "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
   16.62  by(auto simp: distinct_conv_nth)
   16.63  
   16.64 +lemma inj_on_nth: "distinct xs \<Longrightarrow> \<forall>i \<in> I. i < length xs \<Longrightarrow> inj_on (nth xs) I"
   16.65 +by (rule inj_onI) (simp add: nth_eq_iff_index_eq)
   16.66 +
   16.67  lemma set_update_distinct: "\<lbrakk> distinct xs;  n < length xs \<rbrakk> \<Longrightarrow>
   16.68    set(xs[n := x]) = insert x (set xs - {xs!n})"
   16.69  by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
   16.70 @@ -3669,6 +3701,22 @@
   16.71  by (induct xs) simp_all
   16.72  
   16.73  
   16.74 +subsubsection {* @{const List.count} *}
   16.75 +
   16.76 +lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> List.count xs x = 0"
   16.77 +by (induction xs) auto
   16.78 +
   16.79 +lemma count_le_length: "List.count xs x \<le> length xs"
   16.80 +by (induction xs) auto
   16.81 +
   16.82 +lemma setsum_count_set:
   16.83 +  "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (List.count xs) X = length xs"
   16.84 +apply(induction xs arbitrary: X)
   16.85 + apply simp
   16.86 +apply (simp add: setsum.If_cases)
   16.87 +by (metis Diff_eq setsum.remove)
   16.88 +
   16.89 +
   16.90  subsubsection {* @{const List.extract} *}
   16.91  
   16.92  lemma extract_None_iff: "List.extract P xs = None \<longleftrightarrow> \<not> (\<exists> x\<in>set xs. P x)"
    17.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 17 12:23:56 2015 +0000
    17.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 17 14:16:16 2015 +0000
    17.3 @@ -1,4 +1,4 @@
    17.4 -(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
    17.5 +(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
    17.6      Author:     Nik Sultana, Cambridge University Computer Laboratory
    17.7  
    17.8  Various tests for the proof reconstruction module.
    18.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 17 12:23:56 2015 +0000
    18.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 17 14:16:16 2015 +0000
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
    18.5 +(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
    18.6      Author:     Nik Sultana, Cambridge University Computer Laboratory
    18.7  
    18.8  Unit tests for proof reconstruction module.
    19.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 17 12:23:56 2015 +0000
    19.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 17 14:16:16 2015 +0000
    19.3 @@ -26,10 +26,30 @@
    19.4      (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory ->
    19.5      (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
    19.6    val default_comp_sort: (string * sort) list list -> (string * sort) list
    19.7 +  val clean_compose_bnf: BNF_Def.inline_policy -> (binding -> binding) -> binding -> BNF_Def.bnf ->
    19.8 +    BNF_Def.bnf list -> unfold_set * local_theory -> BNF_Def.bnf * (unfold_set * local_theory)
    19.9 +  val kill_bnf: (binding -> binding) -> int -> BNF_Def.bnf ->
   19.10 +    (comp_cache * unfold_set) * local_theory ->
   19.11 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
   19.12 +  val lift_bnf: (binding -> binding) -> int -> BNF_Def.bnf ->
   19.13 +    (comp_cache * unfold_set) * local_theory ->
   19.14 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
   19.15 +  val permute_bnf: (binding -> binding) -> int list -> int list -> BNF_Def.bnf ->
   19.16 +    (comp_cache * unfold_set) * local_theory ->
   19.17 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
   19.18 +  val permute_and_kill_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf ->
   19.19 +    (comp_cache * unfold_set) * local_theory ->
   19.20 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
   19.21 +  val lift_and_permute_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf ->
   19.22 +    (comp_cache * unfold_set) * local_theory ->
   19.23 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
   19.24    val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
   19.25      (''a list list -> ''a list) -> BNF_Def.bnf list -> (comp_cache * unfold_set) * local_theory ->
   19.26      (int list list * ''a list) * (BNF_Def.bnf list * ((comp_cache * unfold_set) * local_theory))
   19.27 -
   19.28 +  val compose_bnf: BNF_Def.inline_policy -> (int -> binding -> binding) ->
   19.29 +    ((string * sort) list list -> (string * sort) list) -> BNF_Def.bnf -> BNF_Def.bnf list ->
   19.30 +    typ list -> typ list list -> typ list list -> (comp_cache * unfold_set) * local_theory ->
   19.31 +    (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
   19.32    type absT_info =
   19.33      {absT: typ,
   19.34       repT: typ,
   19.35 @@ -625,11 +645,11 @@
   19.36  
   19.37  (* Composition pipeline *)
   19.38  
   19.39 -fun permute_and_kill qualify n src dest bnf =
   19.40 +fun permute_and_kill_bnf qualify n src dest bnf =
   19.41    permute_bnf qualify src dest bnf
   19.42    #> uncurry (kill_bnf qualify n);
   19.43  
   19.44 -fun lift_and_permute qualify n src dest bnf =
   19.45 +fun lift_and_permute_bnf qualify n src dest bnf =
   19.46    lift_bnf qualify n bnf
   19.47    #> uncurry (permute_bnf qualify src dest);
   19.48  
   19.49 @@ -641,8 +661,8 @@
   19.50      val before_kill_dest = map2 append kill_poss live_poss;
   19.51      val kill_ns = map length kill_poss;
   19.52      val (inners', accum') =
   19.53 -      @{fold_map 5} (fn i => permute_and_kill (qualify i))
   19.54 -        (if length bnfs = 1 then [0] else (1 upto length bnfs))
   19.55 +      @{fold_map 5} (permute_and_kill_bnf o qualify)
   19.56 +        (if length bnfs = 1 then [0] else 1 upto length bnfs)
   19.57          kill_ns before_kill_src before_kill_dest bnfs accum;
   19.58  
   19.59      val Ass' = map2 (map o nth) Ass live_poss;
   19.60 @@ -653,7 +673,7 @@
   19.61      val after_lift_src = map2 append new_poss old_poss;
   19.62      val lift_ns = map (fn xs => length As - length xs) Ass';
   19.63    in
   19.64 -    ((kill_poss, As), @{fold_map 5} (fn i => lift_and_permute (qualify i))
   19.65 +    ((kill_poss, As), @{fold_map 5} (lift_and_permute_bnf o qualify)
   19.66        (if length bnfs = 1 then [0] else 1 upto length bnfs)
   19.67        lift_ns after_lift_src after_lift_dest inners' accum')
   19.68    end;
   19.69 @@ -881,7 +901,7 @@
   19.70      val map_b = def_qualify (mk_prefix_binding mapN);
   19.71      val rel_b = def_qualify (mk_prefix_binding relN);
   19.72      val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
   19.73 -      else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live);
   19.74 +      else map (def_qualify o mk_prefix_binding o mk_setN) (1 upto live);
   19.75  
   19.76      val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
   19.77        |> map (fn (b, def) => ((b, []), [([def], [])]))
   19.78 @@ -938,7 +958,7 @@
   19.79              val ((inners, (Dss, Ass)), (accum', lthy')) =
   19.80                apfst (apsnd split_list o split_list)
   19.81                  (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
   19.82 -                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
   19.83 +                (if length Ts' = 1 then [0] else 1 upto length Ts') Ts' accum);
   19.84            in
   19.85              compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
   19.86            end)
    20.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 17 12:23:56 2015 +0000
    20.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 17 14:16:16 2015 +0000
    20.3 @@ -81,6 +81,7 @@
    20.4    val rel_mono_of_bnf: bnf -> thm
    20.5    val rel_mono_strong0_of_bnf: bnf -> thm
    20.6    val rel_mono_strong_of_bnf: bnf -> thm
    20.7 +  val rel_refl_of_bnf: bnf -> thm
    20.8    val rel_transfer_of_bnf: bnf -> thm
    20.9    val rel_eq_of_bnf: bnf -> thm
   20.10    val rel_flip_of_bnf: bnf -> thm
   20.11 @@ -250,13 +251,14 @@
   20.12    rel_Grp: thm lazy,
   20.13    rel_conversep: thm lazy,
   20.14    rel_OO: thm lazy,
   20.15 +  rel_refl: thm lazy,
   20.16    rel_transfer: thm lazy
   20.17  };
   20.18  
   20.19  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
   20.20      inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident
   20.21      map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong
   20.22 -    rel_transfer rel_Grp rel_conversep rel_OO set_transfer = {
   20.23 +    set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer = {
   20.24    bd_Card_order = bd_Card_order,
   20.25    bd_Cinfinite = bd_Cinfinite,
   20.26    bd_Cnotzero = bd_Cnotzero,
   20.27 @@ -286,6 +288,7 @@
   20.28    rel_Grp = rel_Grp,
   20.29    rel_conversep = rel_conversep,
   20.30    rel_OO = rel_OO,
   20.31 +  rel_refl = rel_refl,
   20.32    set_transfer = set_transfer};
   20.33  
   20.34  fun map_facts f {
   20.35 @@ -318,6 +321,7 @@
   20.36    rel_Grp,
   20.37    rel_conversep,
   20.38    rel_OO,
   20.39 +  rel_refl,
   20.40    set_transfer} =
   20.41    {bd_Card_order = f bd_Card_order,
   20.42      bd_Cinfinite = f bd_Cinfinite,
   20.43 @@ -348,6 +352,7 @@
   20.44      rel_Grp = Lazy.map f rel_Grp,
   20.45      rel_conversep = Lazy.map f rel_conversep,
   20.46      rel_OO = Lazy.map f rel_OO,
   20.47 +    rel_refl = Lazy.map f rel_refl,
   20.48      set_transfer = Lazy.map (map f) set_transfer};
   20.49  
   20.50  val morph_facts = map_facts o Morphism.thm;
   20.51 @@ -479,6 +484,7 @@
   20.52  val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
   20.53  val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
   20.54  val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
   20.55 +val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
   20.56  val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
   20.57  val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
   20.58  val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
   20.59 @@ -654,14 +660,15 @@
   20.60  val set_map0N = "set_map0";
   20.61  val set_mapN = "set_map";
   20.62  val set_bdN = "set_bd";
   20.63 -val set_transferN = "set_transfer"
   20.64 +val set_transferN = "set_transfer";
   20.65  val rel_GrpN = "rel_Grp";
   20.66  val rel_conversepN = "rel_conversep";
   20.67 -val rel_mapN = "rel_map"
   20.68 -val rel_monoN = "rel_mono"
   20.69 -val rel_mono_strong0N = "rel_mono_strong0"
   20.70 -val rel_mono_strongN = "rel_mono_strong"
   20.71 -val rel_transferN = "rel_transfer"
   20.72 +val rel_mapN = "rel_map";
   20.73 +val rel_monoN = "rel_mono";
   20.74 +val rel_mono_strong0N = "rel_mono_strong0";
   20.75 +val rel_mono_strongN = "rel_mono_strong";
   20.76 +val rel_reflN = "rel_refl";
   20.77 +val rel_transferN = "rel_transfer";
   20.78  val rel_comppN = "rel_compp";
   20.79  val rel_compp_GrpN = "rel_compp_Grp";
   20.80  
   20.81 @@ -732,6 +739,7 @@
   20.82             (rel_mapN, Lazy.force (#rel_map facts), []),
   20.83             (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
   20.84             (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
   20.85 +           (rel_reflN, [Lazy.force (#rel_refl facts)], []),
   20.86             (rel_transferN, [Lazy.force (#rel_transfer facts)], []),
   20.87             (set_mapN, map Lazy.force (#set_map facts), []),
   20.88             (set_transferN, Lazy.force (#set_transfer facts), [])]
   20.89 @@ -1406,6 +1414,11 @@
   20.90  
   20.91          val rel_map = Lazy.lazy mk_rel_map;
   20.92  
   20.93 +        fun mk_rel_refl () = @{thm ge_eq_refl[OF ord_eq_le_trans]} OF
   20.94 +          [Lazy.force rel_eq RS sym, Lazy.force rel_mono OF (replicate live @{thm refl_ge_eq})];
   20.95 +
   20.96 +        val rel_refl = Lazy.lazy mk_rel_refl;
   20.97 +
   20.98          fun mk_map_transfer () =
   20.99            let
  20.100              val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
  20.101 @@ -1494,7 +1507,7 @@
  20.102          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
  20.103            in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
  20.104            map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
  20.105 -          rel_mono_strong rel_transfer rel_Grp rel_conversep rel_OO set_transfer;
  20.106 +          rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer;
  20.107  
  20.108          val wits = map2 mk_witness bnf_wits wit_thms;
  20.109  
    21.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Tue Mar 17 12:23:56 2015 +0000
    21.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Tue Mar 17 14:16:16 2015 +0000
    21.3 @@ -1,4 +1,4 @@
    21.4 -(*  Title:      HOL/Tools/Transfer/transfer_bnf.ML
    21.5 +(*  Title:      HOL/Tools/Lifting/lifting_bnf.ML
    21.6      Author:     Ondrej Kuncar, TU Muenchen
    21.7  
    21.8  Setup for Lifting for types that are BNF.
    22.1 --- a/src/Pure/Concurrent/random.ML	Tue Mar 17 12:23:56 2015 +0000
    22.2 +++ b/src/Pure/Concurrent/random.ML	Tue Mar 17 14:16:16 2015 +0000
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      Pure/Confurrent/random.ML
    22.5 +(*  Title:      Pure/Concurrent/random.ML
    22.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7  
    22.8  Pseudo random numbers.
    23.1 --- a/src/Pure/GUI/jfx_gui.scala	Tue Mar 17 12:23:56 2015 +0000
    23.2 +++ b/src/Pure/GUI/jfx_gui.scala	Tue Mar 17 14:16:16 2015 +0000
    23.3 @@ -1,4 +1,4 @@
    23.4 -/*  Title:      Pure/GUI/jfx_thread.scala
    23.5 +/*  Title:      Pure/GUI/jfx_gui.scala
    23.6      Module:     PIDE-JFX
    23.7      Author:     Makarius
    23.8  
    24.1 --- a/src/Pure/General/antiquote.scala	Tue Mar 17 12:23:56 2015 +0000
    24.2 +++ b/src/Pure/General/antiquote.scala	Tue Mar 17 14:16:16 2015 +0000
    24.3 @@ -1,4 +1,4 @@
    24.4 -/*  Title:      Pure/ML/antiquote.scala
    24.5 +/*  Title:      Pure/General/antiquote.scala
    24.6      Author:     Makarius
    24.7  
    24.8  Antiquotations within plain text.
    25.1 --- a/src/Pure/General/completion.ML	Tue Mar 17 12:23:56 2015 +0000
    25.2 +++ b/src/Pure/General/completion.ML	Tue Mar 17 14:16:16 2015 +0000
    25.3 @@ -1,4 +1,4 @@
    25.4 -(*  Title:      Pure/Isar/completion.ML
    25.5 +(*  Title:      Pure/General/completion.ML
    25.6      Author:     Makarius
    25.7  
    25.8  Semantic completion within the formal context.
    26.1 --- a/src/Pure/General/completion.scala	Tue Mar 17 12:23:56 2015 +0000
    26.2 +++ b/src/Pure/General/completion.scala	Tue Mar 17 14:16:16 2015 +0000
    26.3 @@ -135,10 +135,31 @@
    26.4  
    26.5    /** semantic completion **/
    26.6  
    26.7 +  def report_no_completion(pos: Position.T): String =
    26.8 +    YXML.string_of_tree(Semantic.Info(pos, No_Completion))
    26.9 +
   26.10 +  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
   26.11 +    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
   26.12 +
   26.13    object Semantic
   26.14    {
   26.15      object Info
   26.16      {
   26.17 +      def apply(pos: Position.T, semantic: Semantic): XML.Elem =
   26.18 +      {
   26.19 +        val elem =
   26.20 +          semantic match {
   26.21 +            case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
   26.22 +            case Names(total, names) =>
   26.23 +              XML.Elem(Markup(Markup.COMPLETION, pos),
   26.24 +                {
   26.25 +                  import XML.Encode._
   26.26 +                  pair(int, list(pair(string, pair(string, string))))(total, names)
   26.27 +                })
   26.28 +          }
   26.29 +        XML.Elem(Markup(Markup.REPORT, pos), List(elem))
   26.30 +      }
   26.31 +
   26.32        def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
   26.33          info.info match {
   26.34            case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
    27.1 --- a/src/Pure/Isar/token.scala	Tue Mar 17 12:23:56 2015 +0000
    27.2 +++ b/src/Pure/Isar/token.scala	Tue Mar 17 14:16:16 2015 +0000
    27.3 @@ -161,6 +161,7 @@
    27.4      val start: Pos = new Pos(1, 1, "", "")
    27.5      def file(file: String): Pos = new Pos(1, 1, file, "")
    27.6      def id(id: String): Pos = new Pos(0, 1, "", id)
    27.7 +    val command: Pos = id(Markup.COMMAND)
    27.8    }
    27.9  
   27.10    final class Pos private[Token](
    28.1 --- a/src/Pure/PIDE/batch_session.scala	Tue Mar 17 12:23:56 2015 +0000
    28.2 +++ b/src/Pure/PIDE/batch_session.scala	Tue Mar 17 14:16:16 2015 +0000
    28.3 @@ -1,4 +1,4 @@
    28.4 -/*  Title:      Pure/Tools/batch_session.scala
    28.5 +/*  Title:      Pure/PIDE/batch_session.scala
    28.6      Author:     Makarius
    28.7  
    28.8  PIDE session in batch mode.
    29.1 --- a/src/Pure/PIDE/command.scala	Tue Mar 17 12:23:56 2015 +0000
    29.2 +++ b/src/Pure/PIDE/command.scala	Tue Mar 17 14:16:16 2015 +0000
    29.3 @@ -234,7 +234,7 @@
    29.4                if (Protocol.is_inlined(message)) {
    29.5                  for {
    29.6                    (chunk_name, chunk) <- command.chunks.iterator
    29.7 -                  range <- Protocol.message_positions(
    29.8 +                  range <- Protocol_Message.positions(
    29.9                      self_id, command.position, chunk_name, chunk, message)
   29.10                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
   29.11                }
   29.12 @@ -362,13 +362,15 @@
   29.13        case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
   29.14          val header =
   29.15            resources.check_thy_reader("", node_name,
   29.16 -            new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
   29.17 -        val import_errors =
   29.18 +            new CharSequenceReader(span.source), Token.Pos.command)
   29.19 +        val errors =
   29.20            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
   29.21 -            val name = imp.node
   29.22 -            "Bad theory import " + Markup.Path(name).markup(quote(name)) + Position.here(pos)
   29.23 +            val msg =
   29.24 +              "Bad theory import " +
   29.25 +                Markup.Path(imp.node).markup(quote(imp.toString)) + Position.here(pos)
   29.26 +            Exn.Exn(ERROR(msg)): Command.Blob
   29.27            }
   29.28 -        ((header.errors ::: import_errors).map(msg => Exn.Exn(ERROR(msg)): Command.Blob), -1)
   29.29 +        (errors, -1)
   29.30  
   29.31        // auxiliary files
   29.32        case _ =>
    30.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 17 12:23:56 2015 +0000
    30.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 17 14:16:16 2015 +0000
    30.3 @@ -8,7 +8,7 @@
    30.4  signature DOCUMENT =
    30.5  sig
    30.6    val timing: bool Unsynchronized.ref
    30.7 -  type node_header = string * Thy_Header.header * string list
    30.8 +  type node_header = {master: string, header: Thy_Header.header, errors: string list}
    30.9    type overlay = Document_ID.command * (string * string list)
   30.10    datatype node_edit =
   30.11      Edits of (Document_ID.command option * Document_ID.command option) list |
   30.12 @@ -42,7 +42,8 @@
   30.13  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
   30.14  fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
   30.15  
   30.16 -type node_header = string * Thy_Header.header * string list;
   30.17 +type node_header =
   30.18 +  {master: string, header: Thy_Header.header, errors: string list};
   30.19  
   30.20  type perspective =
   30.21   {required: bool,  (*required node*)
   30.22 @@ -74,7 +75,8 @@
   30.23    visible_last = try List.last command_ids,
   30.24    overlays = Inttab.make_list overlays};
   30.25  
   30.26 -val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
   30.27 +val no_header: node_header =
   30.28 +  {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
   30.29  val no_perspective = make_perspective (false, [], []);
   30.30  
   30.31  val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
   30.32 @@ -95,20 +97,16 @@
   30.33  
   30.34  (* basic components *)
   30.35  
   30.36 -fun master_directory (Node {header = (master, _, _), ...}) =
   30.37 +fun master_directory (Node {header = {master, ...}, ...}) =
   30.38    (case try Url.explode master of
   30.39      SOME (Url.File path) => path
   30.40    | _ => Path.current);
   30.41  
   30.42 -fun set_header header =
   30.43 +fun set_header master header errors =
   30.44    map_node (fn (_, keywords, perspective, entries, result) =>
   30.45 -    (header, keywords, perspective, entries, result));
   30.46 +    ({master = master, header = header, errors = errors}, keywords, perspective, entries, result));
   30.47  
   30.48 -fun get_header_raw (Node {header, ...}) = header;
   30.49 -
   30.50 -fun get_header (Node {header = (master, header, errors), ...}) =
   30.51 -  if null errors then (master, header)
   30.52 -  else error (cat_lines errors);
   30.53 +fun get_header (Node {header, ...}) = header;
   30.54  
   30.55  fun set_keywords keywords =
   30.56    map_node (fn (header, _, perspective, entries, result) =>
   30.57 @@ -118,7 +116,16 @@
   30.58  
   30.59  fun read_header node span =
   30.60    let
   30.61 -    val {name = (name, _), imports, keywords} = #2 (get_header node);
   30.62 +    val {header, errors, ...} = get_header node;
   30.63 +    val _ =
   30.64 +      if null errors then ()
   30.65 +      else
   30.66 +        cat_lines errors |>
   30.67 +        (case Position.get_id (Position.thread_data ()) of
   30.68 +          NONE => I
   30.69 +        | SOME id => Protocol_Message.command_positions_yxml id)
   30.70 +        |> error;
   30.71 +    val {name = (name, _), imports, keywords} = header;
   30.72      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
   30.73    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
   30.74  
   30.75 @@ -232,7 +239,7 @@
   30.76    Version
   30.77      (case node_edit of
   30.78        Edits edits => update_node name (edit_node edits) nodes
   30.79 -    | Deps (master, header, errors) =>
   30.80 +    | Deps {master, header, errors} =>
   30.81          let
   30.82            val imports = map fst (#imports header);
   30.83            val nodes1 = nodes
   30.84 @@ -244,7 +251,7 @@
   30.85            val (nodes3, errors1) =
   30.86              (String_Graph.add_deps_acyclic (name, imports) nodes2, errors)
   30.87                handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs);
   30.88 -        in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end
   30.89 +        in String_Graph.map_node name (set_header master header errors1) nodes3 end
   30.90      | Perspective perspective => update_node name (set_perspective perspective) nodes);
   30.91  
   30.92  fun update_keywords name nodes =
   30.93 @@ -252,7 +259,7 @@
   30.94      if is_empty_node node then node
   30.95      else
   30.96        let
   30.97 -        val (master, header, errors) = get_header_raw node;
   30.98 +        val {master, header, errors} = get_header node;
   30.99          val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header);
  30.100          val keywords =
  30.101            Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords);
  30.102 @@ -262,7 +269,7 @@
  30.103                (keywords, if member (op =) errors msg then errors else errors @ [msg]);
  30.104        in
  30.105          node
  30.106 -        |> set_header (master, header, errors')
  30.107 +        |> set_header master header errors'
  30.108          |> set_keywords (SOME keywords')
  30.109        end);
  30.110  
  30.111 @@ -513,21 +520,29 @@
  30.112      val master_dir = master_directory node;
  30.113      val header = read_header node span;
  30.114      val imports = #imports header;
  30.115 -    val parents =
  30.116 -      imports |> map (fn (import, _) =>
  30.117 +
  30.118 +    fun maybe_end_theory pos st =
  30.119 +      SOME (Toplevel.end_theory pos st)
  30.120 +        handle ERROR msg => (Output.error_message msg; NONE);
  30.121 +    val parents_reports =
  30.122 +      imports |> map_filter (fn (import, pos) =>
  30.123          (case loaded_theory import of
  30.124 -          SOME thy => thy
  30.125 -        | NONE =>
  30.126 -            Toplevel.end_theory (Position.file_only import)
  30.127 +          NONE =>
  30.128 +            maybe_end_theory pos
  30.129                (case get_result (snd (the (AList.lookup (op =) deps import))) of
  30.130                  NONE => Toplevel.toplevel
  30.131 -              | SOME eval => Command.eval_result_state eval)));
  30.132 -    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
  30.133 +              | SOME eval => Command.eval_result_state eval)
  30.134 +        | some => some)
  30.135 +        |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
  30.136 +
  30.137 +    val parents =
  30.138 +      if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports;
  30.139 +    val _ = Position.reports (map #2 parents_reports);
  30.140    in Resources.begin_theory master_dir header parents end;
  30.141  
  30.142  fun check_theory full name node =
  30.143    is_some (loaded_theory name) orelse
  30.144 -  can get_header node andalso (not full orelse is_some (get_result node));
  30.145 +  null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
  30.146  
  30.147  fun last_common keywords state node_required node0 node =
  30.148    let
    31.1 --- a/src/Pure/PIDE/protocol.ML	Tue Mar 17 12:23:56 2015 +0000
    31.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Mar 17 14:16:16 2015 +0000
    31.3 @@ -32,11 +32,15 @@
    31.4        let
    31.5          val (blobs, blobs_index) =
    31.6            YXML.parse_body blobs_yxml |>
    31.7 -            let open XML.Decode in
    31.8 +            let
    31.9 +              val message =
   31.10 +                YXML.string_of_body o Protocol_Message.command_positions id;
   31.11 +              open XML.Decode;
   31.12 +            in
   31.13                pair
   31.14                  (list (variant
   31.15                   [fn ([], a) => Exn.Res (pair string (option string) a),
   31.16 -                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
   31.17 +                  fn ([], a) => Exn.Exn (ERROR (message a))]))
   31.18                  int
   31.19              end;
   31.20          val toks =
   31.21 @@ -78,7 +82,7 @@
   31.22                                (list YXML.string_of_body)))) a;
   31.23                          val imports' = map (rpair Position.none) imports;
   31.24                          val header = Thy_Header.make (name, Position.none) imports' keywords;
   31.25 -                      in Document.Deps (master, header, errors) end,
   31.26 +                      in Document.Deps {master = master, header = header, errors = errors} end,
   31.27                      fn (a :: b, c) =>
   31.28                        Document.Perspective (bool_atom a, map int_atom b,
   31.29                          list (pair int (pair string (list string))) c)]))
    32.1 --- a/src/Pure/PIDE/protocol.scala	Tue Mar 17 12:23:56 2015 +0000
    32.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 17 14:16:16 2015 +0000
    32.3 @@ -186,34 +186,6 @@
    32.4  
    32.5    /* result messages */
    32.6  
    32.7 -  private val clean_elements =
    32.8 -    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    32.9 -
   32.10 -  def clean_message(body: XML.Body): XML.Body =
   32.11 -    body filter {
   32.12 -      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
   32.13 -      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
   32.14 -      case _ => true
   32.15 -    } map {
   32.16 -      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
   32.17 -      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
   32.18 -      case t => t
   32.19 -    }
   32.20 -
   32.21 -  def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
   32.22 -    body flatMap {
   32.23 -      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
   32.24 -        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
   32.25 -      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
   32.26 -        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
   32.27 -      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
   32.28 -      case XML.Elem(_, ts) => message_reports(props, ts)
   32.29 -      case XML.Text(_) => Nil
   32.30 -    }
   32.31 -
   32.32 -
   32.33 -  /* specific messages */
   32.34 -
   32.35    def is_result(msg: XML.Tree): Boolean =
   32.36      msg match {
   32.37        case XML.Elem(Markup(Markup.RESULT, _), _) => true
   32.38 @@ -302,53 +274,6 @@
   32.39          case _ => None
   32.40        }
   32.41    }
   32.42 -
   32.43 -
   32.44 -  /* reported positions */
   32.45 -
   32.46 -  private val position_elements =
   32.47 -    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   32.48 -
   32.49 -  def message_positions(
   32.50 -    self_id: Document_ID.Generic => Boolean,
   32.51 -    command_position: Position.T,
   32.52 -    chunk_name: Symbol.Text_Chunk.Name,
   32.53 -    chunk: Symbol.Text_Chunk,
   32.54 -    message: XML.Elem): Set[Text.Range] =
   32.55 -  {
   32.56 -    def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
   32.57 -      props match {
   32.58 -        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
   32.59 -          val opt_range =
   32.60 -            Position.Range.unapply(props) orElse {
   32.61 -              if (name == Symbol.Text_Chunk.Default)
   32.62 -                Position.Range.unapply(command_position)
   32.63 -              else None
   32.64 -            }
   32.65 -          opt_range match {
   32.66 -            case Some(symbol_range) =>
   32.67 -              chunk.incorporate(symbol_range) match {
   32.68 -                case Some(range) => set + range
   32.69 -                case _ => set
   32.70 -              }
   32.71 -            case None => set
   32.72 -          }
   32.73 -        case _ => set
   32.74 -      }
   32.75 -
   32.76 -    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
   32.77 -      tree match {
   32.78 -        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
   32.79 -          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
   32.80 -        case XML.Elem(Markup(name, props), body) =>
   32.81 -          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
   32.82 -        case XML.Text(_) => set
   32.83 -      }
   32.84 -
   32.85 -    val set = positions(Set.empty, message)
   32.86 -    if (set.isEmpty) elem_positions(message.markup.properties, set)
   32.87 -    else set
   32.88 -  }
   32.89  }
   32.90  
   32.91  
   32.92 @@ -382,29 +307,6 @@
   32.93    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
   32.94      protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
   32.95  
   32.96 -  private def resolve_id(id: String, body: XML.Body): XML.Body =
   32.97 -  {
   32.98 -    def resolve_property(p: (String, String)): (String, String) =
   32.99 -      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
  32.100 -
  32.101 -    def resolve_markup(markup: Markup): Markup =
  32.102 -      Markup(markup.name, markup.properties.map(resolve_property))
  32.103 -
  32.104 -    def resolve_tree(t: XML.Tree): XML.Tree =
  32.105 -      t match {
  32.106 -        case XML.Wrapped_Elem(markup, ts1, ts2) =>
  32.107 -          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
  32.108 -        case XML.Elem(markup, ts) =>
  32.109 -          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
  32.110 -        case text => text
  32.111 -      }
  32.112 -    body.map(resolve_tree _)
  32.113 -  }
  32.114 -
  32.115 -  private def resolve_id(id: String, s: String): XML.Body =
  32.116 -    try { resolve_id(id, YXML.parse_body(s)) }
  32.117 -    catch { case ERROR(_) => XML.Encode.string(s) }
  32.118 -
  32.119    def define_command(command: Command)
  32.120    {
  32.121      val blobs_yxml =
  32.122 @@ -413,7 +315,7 @@
  32.123          variant(List(
  32.124            { case Exn.Res((a, b)) =>
  32.125                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
  32.126 -          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
  32.127 +          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
  32.128  
  32.129        YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
  32.130      }
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/Pure/PIDE/protocol_message.ML	Tue Mar 17 14:16:16 2015 +0000
    33.3 @@ -0,0 +1,27 @@
    33.4 +(*  Title:      Pure/PIDE/protocol_message.ML
    33.5 +    Author:     Makarius
    33.6 +
    33.7 +Auxiliary operations on protocol messages.
    33.8 +*)
    33.9 +
   33.10 +signature PROTOCOL_MESSAGE =
   33.11 +sig
   33.12 +  val command_positions: string -> XML.body -> XML.body
   33.13 +  val command_positions_yxml: string -> string -> string
   33.14 +end;
   33.15 +
   33.16 +structure Protocol_Message: PROTOCOL_MESSAGE =
   33.17 +struct
   33.18 +
   33.19 +fun command_positions id =
   33.20 +  let
   33.21 +    fun attribute (a, b) =
   33.22 +      if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
   33.23 +    fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
   33.24 +      | tree text = text;
   33.25 +  in map tree end;
   33.26 +
   33.27 +fun command_positions_yxml id =
   33.28 +  YXML.string_of_body o command_positions id o YXML.parse_body;
   33.29 +
   33.30 +end;
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/src/Pure/PIDE/protocol_message.scala	Tue Mar 17 14:16:16 2015 +0000
    34.3 @@ -0,0 +1,84 @@
    34.4 +/*  Title:      Pure/PIDE/protocol_message.scala
    34.5 +    Author:     Makarius
    34.6 +
    34.7 +Auxiliary operations on protocol messages.
    34.8 +*/
    34.9 +
   34.10 +package isabelle
   34.11 +
   34.12 +
   34.13 +object Protocol_Message
   34.14 +{
   34.15 +  /* inlined reports */
   34.16 +
   34.17 +  private val report_elements =
   34.18 +    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
   34.19 +
   34.20 +  def clean_reports(body: XML.Body): XML.Body =
   34.21 +    body filter {
   34.22 +      case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
   34.23 +      case XML.Elem(Markup(name, _), _) => !report_elements(name)
   34.24 +      case _ => true
   34.25 +    } map {
   34.26 +      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
   34.27 +      case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
   34.28 +      case t => t
   34.29 +    }
   34.30 +
   34.31 +  def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
   34.32 +    body flatMap {
   34.33 +      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
   34.34 +        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
   34.35 +      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
   34.36 +        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
   34.37 +      case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
   34.38 +      case XML.Elem(_, ts) => reports(props, ts)
   34.39 +      case XML.Text(_) => Nil
   34.40 +    }
   34.41 +
   34.42 +
   34.43 +  /* reported positions */
   34.44 +
   34.45 +  private val position_elements =
   34.46 +    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   34.47 +
   34.48 +  def positions(
   34.49 +    self_id: Document_ID.Generic => Boolean,
   34.50 +    command_position: Position.T,
   34.51 +    chunk_name: Symbol.Text_Chunk.Name,
   34.52 +    chunk: Symbol.Text_Chunk,
   34.53 +    message: XML.Elem): Set[Text.Range] =
   34.54 +  {
   34.55 +    def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
   34.56 +      props match {
   34.57 +        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
   34.58 +          val opt_range =
   34.59 +            Position.Range.unapply(props) orElse {
   34.60 +              if (name == Symbol.Text_Chunk.Default)
   34.61 +                Position.Range.unapply(command_position)
   34.62 +              else None
   34.63 +            }
   34.64 +          opt_range match {
   34.65 +            case Some(symbol_range) =>
   34.66 +              chunk.incorporate(symbol_range) match {
   34.67 +                case Some(range) => set + range
   34.68 +                case _ => set
   34.69 +              }
   34.70 +            case None => set
   34.71 +          }
   34.72 +        case _ => set
   34.73 +      }
   34.74 +    def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
   34.75 +      t match {
   34.76 +        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
   34.77 +          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
   34.78 +        case XML.Elem(Markup(name, props), body) =>
   34.79 +          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
   34.80 +        case XML.Text(_) => set
   34.81 +      }
   34.82 +
   34.83 +    val set = tree(Set.empty, message)
   34.84 +    if (set.isEmpty) elem(message.markup.properties, set)
   34.85 +    else set
   34.86 +  }
   34.87 +}
    35.1 --- a/src/Pure/PIDE/prover.scala	Tue Mar 17 12:23:56 2015 +0000
    35.2 +++ b/src/Pure/PIDE/prover.scala	Tue Mar 17 14:16:16 2015 +0000
    35.3 @@ -108,8 +108,8 @@
    35.4    {
    35.5      if (kind == Markup.INIT) system_channel.accepted()
    35.6  
    35.7 -    val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
    35.8 -    val reports = Protocol.message_reports(props, body)
    35.9 +    val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
   35.10 +    val reports = Protocol_Message.reports(props, body)
   35.11      for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   35.12    }
   35.13  
    36.1 --- a/src/Pure/PIDE/resources.ML	Tue Mar 17 12:23:56 2015 +0000
    36.2 +++ b/src/Pure/PIDE/resources.ML	Tue Mar 17 14:16:16 2015 +0000
    36.3 @@ -68,7 +68,8 @@
    36.4      val {name = (name, pos), imports, keywords} =
    36.5        Thy_Header.read (Path.position master_file) text;
    36.6      val _ = thy_name <> name andalso
    36.7 -      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
    36.8 +      error ("Bad theory name " ^ quote name ^
    36.9 +        " for file " ^ Path.print path ^ Position.here pos);
   36.10    in
   36.11     {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
   36.12      imports = imports, keywords = keywords}
    37.1 --- a/src/Pure/PIDE/resources.scala	Tue Mar 17 12:23:56 2015 +0000
    37.2 +++ b/src/Pure/PIDE/resources.scala	Tue Mar 17 14:16:16 2015 +0000
    37.3 @@ -96,8 +96,9 @@
    37.4          val base_name = Long_Name.base_name(node_name.theory)
    37.5          val (name, pos) = header.name
    37.6          if (base_name != name)
    37.7 -          error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
    37.8 -            " for theory " + quote(name) + Position.here(pos))
    37.9 +          error("Bad theory name " + quote(name) +
   37.10 +            " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) +
   37.11 +            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
   37.12  
   37.13          val imports =
   37.14            header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
    38.1 --- a/src/Pure/ROOT	Tue Mar 17 12:23:56 2015 +0000
    38.2 +++ b/src/Pure/ROOT	Tue Mar 17 14:16:16 2015 +0000
    38.3 @@ -172,6 +172,7 @@
    38.4      "PIDE/execution.ML"
    38.5      "PIDE/markup.ML"
    38.6      "PIDE/protocol.ML"
    38.7 +    "PIDE/protocol_message.ML"
    38.8      "PIDE/query_operation.ML"
    38.9      "PIDE/resources.ML"
   38.10      "PIDE/session.ML"
    39.1 --- a/src/Pure/ROOT.ML	Tue Mar 17 12:23:56 2015 +0000
    39.2 +++ b/src/Pure/ROOT.ML	Tue Mar 17 14:16:16 2015 +0000
    39.3 @@ -310,6 +310,7 @@
    39.4  use "PIDE/resources.ML";
    39.5  use "Thy/thy_info.ML";
    39.6  use "PIDE/session.ML";
    39.7 +use "PIDE/protocol_message.ML";
    39.8  use "PIDE/document.ML";
    39.9  
   39.10  (*theory and proof operations*)
    40.1 --- a/src/Pure/System/posix_interrupt.scala	Tue Mar 17 12:23:56 2015 +0000
    40.2 +++ b/src/Pure/System/posix_interrupt.scala	Tue Mar 17 14:16:16 2015 +0000
    40.3 @@ -1,4 +1,4 @@
    40.4 -/*  Title:      Pure/System/interrupt.scala
    40.5 +/*  Title:      Pure/System/posix_interrupt.scala
    40.6      Author:     Makarius
    40.7  
    40.8  Support for POSIX interrupts (bypassed on Windows).
    41.1 --- a/src/Pure/Tools/build.scala	Tue Mar 17 12:23:56 2015 +0000
    41.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 17 14:16:16 2015 +0000
    41.3 @@ -744,7 +744,7 @@
    41.4    {
    41.5      /* session tree and dependencies */
    41.6  
    41.7 -    val full_tree = find_sessions(options, dirs, select_dirs)
    41.8 +    val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
    41.9      val (selected, selected_tree) =
   41.10        full_tree.selection(requirements, all_sessions, session_groups, sessions)
   41.11  
    42.1 --- a/src/Pure/Tools/print_operation.scala	Tue Mar 17 12:23:56 2015 +0000
    42.2 +++ b/src/Pure/Tools/print_operation.scala	Tue Mar 17 14:16:16 2015 +0000
    42.3 @@ -1,4 +1,4 @@
    42.4 -/*  Title:      Pure/System/print_operation.scala
    42.5 +/*  Title:      Pure/Tools/print_operation.scala
    42.6      Author:     Makarius
    42.7  
    42.8  Print operations as asynchronous query.
    43.1 --- a/src/Pure/build-jars	Tue Mar 17 12:23:56 2015 +0000
    43.2 +++ b/src/Pure/build-jars	Tue Mar 17 14:16:16 2015 +0000
    43.3 @@ -64,6 +64,7 @@
    43.4    PIDE/markup.scala
    43.5    PIDE/markup_tree.scala
    43.6    PIDE/protocol.scala
    43.7 +  PIDE/protocol_message.scala
    43.8    PIDE/prover.scala
    43.9    PIDE/query_operation.scala
   43.10    PIDE/resources.scala
    44.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 12:23:56 2015 +0000
    44.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 14:16:16 2015 +0000
    44.3 @@ -80,7 +80,7 @@
    44.4        JEdit_Lib.buffer_lock(buffer) {
    44.5          Exn.capture {
    44.6            PIDE.resources.check_thy_reader("", node_name,
    44.7 -            JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
    44.8 +            JEdit_Lib.buffer_reader(buffer), Token.Pos.command)
    44.9          } match {
   44.10            case Exn.Res(header) => header
   44.11            case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))