merged
authorAngeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
Mon Sep 03 13:32:29 2018 +0100 (9 months ago)
changeset 688913cdde2ea2667
parent 68890 725d5ed56563
parent 68889 d9c051e9da2b
child 68893 58bf801d679a
merged
     1.1 --- a/NEWS	Mon Sep 03 13:28:52 2018 +0100
     1.2 +++ b/NEWS	Mon Sep 03 13:32:29 2018 +0100
     1.3 @@ -14,6 +14,12 @@
     1.4  specified in seconds; a negative value means it is disabled (default).
     1.5  
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* More robust treatment of structural errors: begin/end blocks take
    1.10 +precedence over goal/proof.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Simplified syntax setup for big operators under image. In rare
    1.16 @@ -22,6 +28,9 @@
    1.17  SUPREMUM, UNION, INTER should now rarely occur in output and are just
    1.18  retained as migration auxiliary. INCOMPATIBILITY.
    1.19  
    1.20 +* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
    1.21 +provers, has been updated.
    1.22 +
    1.23  
    1.24  *** ML ***
    1.25  
    1.26 @@ -49,6 +58,14 @@
    1.27  observes the official standard).
    1.28  
    1.29  
    1.30 +*** System ***
    1.31 +
    1.32 +* Isabelle Server message "use_theories" terminates more robustly in the
    1.33 +presence of structurally broken sources: full consolidation of theories
    1.34 +is no longer required.
    1.35 +
    1.36 +
    1.37 +
    1.38  New in Isabelle2018 (August 2018)
    1.39  ---------------------------------
    1.40  
     2.1 --- a/src/Doc/System/Server.thy	Mon Sep 03 13:28:52 2018 +0100
     2.2 +++ b/src/Doc/System/Server.thy	Mon Sep 03 13:32:29 2018 +0100
     2.3 @@ -516,14 +516,21 @@
     2.4    session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
     2.5  
     2.6    \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
     2.7 -  int, warned: int, failed: int, finished: int, initialized: bool,
     2.8 -  consolidated: bool}\<close> represents a formal theory node status of the PIDE
     2.9 -  document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
    2.10 -  \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
    2.11 -  \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>initialized\<close> flag indicates
    2.12 -  that the initial \<^theory_text>\<open>theory\<close> command has been processed. The \<open>consolidated\<close>
    2.13 -  flag indicates whether the outermost theory command structure has finished
    2.14 -  (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
    2.15 +  int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
    2.16 +  bool}\<close> represents a formal theory node status of the PIDE document model as
    2.17 +  follows.
    2.18 +
    2.19 +    \<^item> Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close>
    2.20 +      account for individual commands within a theory node; \<open>ok\<close> is an
    2.21 +      abstraction for \<open>failed = 0\<close>.
    2.22 +
    2.23 +    \<^item> The \<open>canceled\<close> flag tells if some command in the theory has been
    2.24 +      spontaneously canceled (by an Interrupt exception that could also
    2.25 +      indicate resource problems).
    2.26 +
    2.27 +    \<^item> The \<open>consolidated\<close> flag indicates whether the outermost theory command
    2.28 +    structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been
    2.29 +    checked.
    2.30  \<close>
    2.31  
    2.32  
    2.33 @@ -916,10 +923,9 @@
    2.34    \<^medskip>
    2.35    The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
    2.36    current version of theory files to it, while dependencies are resolved
    2.37 -  implicitly. The command succeeds eventually, when all theories have been
    2.38 -  \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
    2.39 -  (\secref{sec:json-types}): the outermost command structure has finished (or
    2.40 -  failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
    2.41 +  implicitly. The command succeeds eventually, when all theories have status
    2.42 +  \<^emph>\<open>terminated\<close> or \<^emph>\<open>consolidated\<close> in the sense of \<open>node_status\<close>
    2.43 +  (\secref{sec:json-types}).
    2.44  
    2.45    Already used theories persist in the session until purged explicitly
    2.46    (\secref{sec:command-purge-theories}). This also means that repeated
    2.47 @@ -935,14 +941,10 @@
    2.48    represented as plain text in UTF-8 encoding, which means the string needs to
    2.49    be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
    2.50  
    2.51 -  \<^medskip> Due to asynchronous nature of PIDE document processing, structurally
    2.52 -  broken theories never reach the \<open>consolidated\<close> state: consequently
    2.53 -  \<^verbatim>\<open>use_theories\<close> will wait forever. The status is checked every \<open>check_delay\<close>
    2.54 -  seconds, and bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\
    2.55 -  unbounded). A \<open>check_limit > 0\<close> effectively specifies a timeout of
    2.56 -  \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
    2.57 -  option @{system_option editor_consolidate_delay} to give PIDE processing a
    2.58 -  chance to consolidate document nodes in the first place.
    2.59 +  \<^medskip> The status of PIDE processing is checked every \<open>check_delay\<close> seconds, and
    2.60 +  bounded by \<open>check_limit\<close> attempts (default: 0, i.e.\ unbounded). A
    2.61 +  \<open>check_limit > 0\<close> effectively specifies a timeout of \<open>check_delay \<times>
    2.62 +  check_limit\<close> seconds.
    2.63  
    2.64    \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
    2.65    kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
     3.1 --- a/src/HOL/Complete_Lattices.thy	Mon Sep 03 13:28:52 2018 +0100
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Sep 03 13:32:29 2018 +0100
     3.3 @@ -236,6 +236,9 @@
     3.4  lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)"
     3.5    using Inf_mono [of "g ` B" "f ` A"] by auto
     3.6  
     3.7 +lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:A. g x)"
     3.8 +  by (rule INF_mono) auto
     3.9 +
    3.10  lemma Sup_mono:
    3.11    assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
    3.12    shows "\<Squnion>A \<le> \<Squnion>B"
    3.13 @@ -249,6 +252,9 @@
    3.14  lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)"
    3.15    using Sup_mono [of "f ` A" "g ` B"] by auto
    3.16  
    3.17 +lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:A. g x)"
    3.18 +  by (rule SUP_mono) auto
    3.19 +
    3.20  lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)"
    3.21    \<comment> \<open>The last inclusion is POSITIVE!\<close>
    3.22    by (blast intro: INF_mono dest: subsetD)
     4.1 --- a/src/HOL/Filter.thy	Mon Sep 03 13:28:52 2018 +0100
     4.2 +++ b/src/HOL/Filter.thy	Mon Sep 03 13:32:29 2018 +0100
     4.3 @@ -522,6 +522,33 @@
     4.4  lemma eventually_INF1: "i \<in> I \<Longrightarrow> eventually P (F i) \<Longrightarrow> eventually P (\<Sqinter>i\<in>I. F i)"
     4.5    using filter_leD[OF INF_lower] .
     4.6  
     4.7 +lemma eventually_INF_finite:
     4.8 +  assumes "finite A"
     4.9 +  shows   "eventually P (INF x:A. F x) \<longleftrightarrow>
    4.10 +             (\<exists>Q. (\<forall>x\<in>A. eventually (Q x) (F x)) \<and> (\<forall>y. (\<forall>x\<in>A. Q x y) \<longrightarrow> P y))" 
    4.11 +  using assms
    4.12 +proof (induction arbitrary: P rule: finite_induct)
    4.13 +  case (insert a A P)
    4.14 +  from insert.hyps have [simp]: "x \<noteq> a" if "x \<in> A" for x
    4.15 +    using that by auto
    4.16 +  have "eventually P (INF x:insert a A. F x) \<longleftrightarrow>
    4.17 +          (\<exists>Q R S. eventually Q (F a) \<and> (( (\<forall>x\<in>A. eventually (S x) (F x)) \<and>
    4.18 +            (\<forall>y. (\<forall>x\<in>A. S x y) \<longrightarrow> R y)) \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x)))"
    4.19 +    unfolding ex_simps by (simp add: eventually_inf insert.IH)
    4.20 +  also have "\<dots> \<longleftrightarrow> (\<exists>Q. (\<forall>x\<in>insert a A. eventually (Q x) (F x)) \<and>
    4.21 +                           (\<forall>y. (\<forall>x\<in>insert a A. Q x y) \<longrightarrow> P y))"
    4.22 +  proof (safe, goal_cases)
    4.23 +    case (1 Q R S)
    4.24 +    thus ?case using 1 by (intro exI[of _ "S(a := Q)"]) auto
    4.25 +  next
    4.26 +    case (2 Q)
    4.27 +    show ?case
    4.28 +      by (rule exI[of _ "Q a"], rule exI[of _ "\<lambda>y. \<forall>x\<in>A. Q x y"],
    4.29 +          rule exI[of _ "Q(a := (\<lambda>_. True))"]) (use 2 in auto)
    4.30 +  qed
    4.31 +  finally show ?case .
    4.32 +qed auto
    4.33 +
    4.34  subsubsection \<open>Map function for filters\<close>
    4.35  
    4.36  definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
    4.37 @@ -653,6 +680,33 @@
    4.38    "filtercomap f (\<Squnion>b\<in>B. F b) \<ge> (\<Squnion>b\<in>B. filtercomap f (F b))"
    4.39    by (intro SUP_least filtercomap_mono SUP_upper)
    4.40  
    4.41 +lemma filtermap_le_iff_le_filtercomap: "filtermap f F \<le> G \<longleftrightarrow> F \<le> filtercomap f G"
    4.42 +  unfolding le_filter_def eventually_filtermap eventually_filtercomap
    4.43 +  using eventually_mono by auto
    4.44 +
    4.45 +lemma filtercomap_neq_bot:
    4.46 +  assumes "\<And>P. eventually P F \<Longrightarrow> \<exists>x. P (f x)"
    4.47 +  shows   "filtercomap f F \<noteq> bot"
    4.48 +  using assms by (auto simp: trivial_limit_def eventually_filtercomap)
    4.49 +
    4.50 +lemma filtercomap_neq_bot_surj:
    4.51 +  assumes "F \<noteq> bot" and "surj f"
    4.52 +  shows   "filtercomap f F \<noteq> bot"
    4.53 +proof (rule filtercomap_neq_bot)
    4.54 +  fix P assume *: "eventually P F"
    4.55 +  show "\<exists>x. P (f x)"
    4.56 +  proof (rule ccontr)
    4.57 +    assume **: "\<not>(\<exists>x. P (f x))"
    4.58 +    from * have "eventually (\<lambda>_. False) F"
    4.59 +    proof eventually_elim
    4.60 +      case (elim x)
    4.61 +      from \<open>surj f\<close> obtain y where "x = f y" by auto
    4.62 +      with elim and ** show False by auto
    4.63 +    qed
    4.64 +    with assms show False by (simp add: trivial_limit_def)
    4.65 +  qed
    4.66 +qed
    4.67 +
    4.68  lemma eventually_filtercomapI [intro]:
    4.69    assumes "eventually P F"
    4.70    shows   "eventually (\<lambda>x. P (f x)) (filtercomap f F)"
    4.71 @@ -858,6 +912,74 @@
    4.72  lemma filtermap_sequentually_ne_bot: "filtermap f sequentially \<noteq> bot"
    4.73    by (simp add: filtermap_bot_iff)
    4.74  
    4.75 +subsection \<open>Increasing finite subsets\<close>
    4.76 +
    4.77 +definition finite_subsets_at_top where
    4.78 +  "finite_subsets_at_top A = (INF X:{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
    4.79 +
    4.80 +lemma eventually_finite_subsets_at_top:
    4.81 +  "eventually P (finite_subsets_at_top A) \<longleftrightarrow>
    4.82 +     (\<exists>X. finite X \<and> X \<subseteq> A \<and> (\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y))"
    4.83 +  unfolding finite_subsets_at_top_def
    4.84 +proof (subst eventually_INF_base, goal_cases)
    4.85 +  show "{X. finite X \<and> X \<subseteq> A} \<noteq> {}" by auto
    4.86 +next
    4.87 +  case (2 B C)
    4.88 +  thus ?case by (intro bexI[of _ "B \<union> C"]) auto
    4.89 +qed (simp_all add: eventually_principal)
    4.90 +
    4.91 +lemma eventually_finite_subsets_at_top_weakI [intro]:
    4.92 +  assumes "\<And>X. finite X \<Longrightarrow> X \<subseteq> A \<Longrightarrow> P X"
    4.93 +  shows   "eventually P (finite_subsets_at_top A)"
    4.94 +proof -
    4.95 +  have "eventually (\<lambda>X. finite X \<and> X \<subseteq> A) (finite_subsets_at_top A)"
    4.96 +    by (auto simp: eventually_finite_subsets_at_top)
    4.97 +  thus ?thesis by eventually_elim (use assms in auto)
    4.98 +qed
    4.99 +
   4.100 +lemma finite_subsets_at_top_neq_bot [simp]: "finite_subsets_at_top A \<noteq> bot"
   4.101 +proof -
   4.102 +  have "\<not>eventually (\<lambda>x. False) (finite_subsets_at_top A)"
   4.103 +    by (auto simp: eventually_finite_subsets_at_top)
   4.104 +  thus ?thesis by auto
   4.105 +qed
   4.106 +
   4.107 +lemma filtermap_image_finite_subsets_at_top:
   4.108 +  assumes "inj_on f A"
   4.109 +  shows   "filtermap ((`) f) (finite_subsets_at_top A) = finite_subsets_at_top (f ` A)"
   4.110 +  unfolding filter_eq_iff eventually_filtermap
   4.111 +proof (safe, goal_cases)
   4.112 +  case (1 P)
   4.113 +  then obtain X where X: "finite X" "X \<subseteq> A" "\<And>Y. finite Y \<Longrightarrow> X \<subseteq> Y \<Longrightarrow> Y \<subseteq> A \<Longrightarrow> P (f ` Y)"
   4.114 +    unfolding eventually_finite_subsets_at_top by force
   4.115 +  show ?case unfolding eventually_finite_subsets_at_top eventually_filtermap
   4.116 +  proof (rule exI[of _ "f ` X"], intro conjI allI impI, goal_cases)
   4.117 +    case (3 Y)
   4.118 +    with assms and X(1,2) have "P (f ` (f -` Y \<inter> A))" using X(1,2)
   4.119 +      by (intro X(3) finite_vimage_IntI) auto
   4.120 +    also have "f ` (f -` Y \<inter> A) = Y" using assms 3 by blast
   4.121 +    finally show ?case .
   4.122 +  qed (insert assms X(1,2), auto intro!: finite_vimage_IntI)
   4.123 +next
   4.124 +  case (2 P)
   4.125 +  then obtain X where X: "finite X" "X \<subseteq> f ` A" "\<And>Y. finite Y \<Longrightarrow> X \<subseteq> Y \<Longrightarrow> Y \<subseteq> f ` A \<Longrightarrow> P Y"
   4.126 +    unfolding eventually_finite_subsets_at_top by force
   4.127 +  show ?case unfolding eventually_finite_subsets_at_top eventually_filtermap
   4.128 +  proof (rule exI[of _ "f -` X \<inter> A"], intro conjI allI impI, goal_cases)
   4.129 +    case (3 Y)
   4.130 +    with X(1,2) and assms show ?case by (intro X(3)) force+
   4.131 +  qed (insert assms X(1), auto intro!: finite_vimage_IntI)
   4.132 +qed
   4.133 +
   4.134 +lemma eventually_finite_subsets_at_top_finite:
   4.135 +  assumes "finite A"
   4.136 +  shows   "eventually P (finite_subsets_at_top A) \<longleftrightarrow> P A"
   4.137 +  unfolding eventually_finite_subsets_at_top using assms by force
   4.138 +
   4.139 +lemma finite_subsets_at_top_finite: "finite A \<Longrightarrow> finite_subsets_at_top A = principal {A}"
   4.140 +  by (auto simp: filter_eq_iff eventually_finite_subsets_at_top_finite eventually_principal)
   4.141 +
   4.142 +
   4.143  subsection \<open>The cofinite filter\<close>
   4.144  
   4.145  definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
   4.146 @@ -1208,6 +1330,9 @@
   4.147    "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   4.148    unfolding filterlim_def eventually_filtermap le_principal ..
   4.149  
   4.150 +lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
   4.151 +  unfolding filterlim_def by (rule filtermap_filtercomap)
   4.152 +
   4.153  lemma filterlim_inf:
   4.154    "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   4.155    unfolding filterlim_def by simp
   4.156 @@ -1220,6 +1345,15 @@
   4.157    "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (\<Sqinter>i\<in>I. F i). f x :> (\<Sqinter>j\<in>J. G j)"
   4.158    unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
   4.159  
   4.160 +lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (INF x:A. G x)"
   4.161 +  unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]])
   4.162 +
   4.163 +lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F \<longleftrightarrow> filterlim (g \<circ> f) G F"
   4.164 +  by (simp add: filterlim_def filtermap_le_iff_le_filtercomap filtercomap_filtercomap o_def)
   4.165 +
   4.166 +lemma filterlim_iff_le_filtercomap: "filterlim f F G \<longleftrightarrow> G \<le> filtercomap f F"
   4.167 +  by (simp add: filterlim_def filtermap_le_iff_le_filtercomap)
   4.168 +
   4.169  lemma filterlim_base:
   4.170    "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
   4.171      LIM x (\<Sqinter>i\<in>I. principal (F i)). f x :> (\<Sqinter>j\<in>J. principal (G j))"
   4.172 @@ -1347,9 +1481,51 @@
   4.173    shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   4.174    by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   4.175      
   4.176 -lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
   4.177 -  unfolding filterlim_def by (rule filtermap_filtercomap)
   4.178 +lemma filterlim_finite_subsets_at_top:
   4.179 +  "filterlim f (finite_subsets_at_top A) F \<longleftrightarrow>
   4.180 +     (\<forall>X. finite X \<and> X \<subseteq> A \<longrightarrow> eventually (\<lambda>y. finite (f y) \<and> X \<subseteq> f y \<and> f y \<subseteq> A) F)"
   4.181 +  (is "?lhs = ?rhs")
   4.182 +proof 
   4.183 +  assume ?lhs
   4.184 +  thus ?rhs
   4.185 +  proof (safe, goal_cases)
   4.186 +    case (1 X)
   4.187 +    hence *: "(\<forall>\<^sub>F x in F. P (f x))" if "eventually P (finite_subsets_at_top A)" for P
   4.188 +      using that by (auto simp: filterlim_def le_filter_def eventually_filtermap)
   4.189 +    have "\<forall>\<^sub>F Y in finite_subsets_at_top A. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A"
   4.190 +      using 1 unfolding eventually_finite_subsets_at_top by force
   4.191 +    thus ?case by (intro *) auto
   4.192 +  qed
   4.193 +next
   4.194 +  assume rhs: ?rhs
   4.195 +  show ?lhs unfolding filterlim_def le_filter_def eventually_finite_subsets_at_top
   4.196 +  proof (safe, goal_cases)
   4.197 +    case (1 P X)
   4.198 +    with rhs have "\<forall>\<^sub>F y in F. finite (f y) \<and> X \<subseteq> f y \<and> f y \<subseteq> A" by auto
   4.199 +    thus "eventually P (filtermap f F)" unfolding eventually_filtermap
   4.200 +      by eventually_elim (insert 1, auto)
   4.201 +  qed
   4.202 +qed
   4.203  
   4.204 +lemma filterlim_atMost_at_top:
   4.205 +  "filterlim (\<lambda>n. {..n}) (finite_subsets_at_top (UNIV :: nat set)) at_top"
   4.206 +  unfolding filterlim_finite_subsets_at_top
   4.207 +proof (safe, goal_cases)
   4.208 +  case (1 X)
   4.209 +  then obtain n where n: "X \<subseteq> {..n}" by (auto simp: finite_nat_set_iff_bounded_le)
   4.210 +  show ?case using eventually_ge_at_top[of n]
   4.211 +    by eventually_elim (insert n, auto)
   4.212 +qed
   4.213 +
   4.214 +lemma filterlim_lessThan_at_top:
   4.215 +  "filterlim (\<lambda>n. {..<n}) (finite_subsets_at_top (UNIV :: nat set)) at_top"
   4.216 +  unfolding filterlim_finite_subsets_at_top
   4.217 +proof (safe, goal_cases)
   4.218 +  case (1 X)
   4.219 +  then obtain n where n: "X \<subseteq> {..<n}" by (auto simp: finite_nat_set_iff_bounded)
   4.220 +  show ?case using eventually_ge_at_top[of n]
   4.221 +    by eventually_elim (insert n, auto)
   4.222 +qed
   4.223  
   4.224  subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
   4.225  
     5.1 --- a/src/HOL/Library/Countable_Set.thy	Mon Sep 03 13:28:52 2018 +0100
     5.2 +++ b/src/HOL/Library/Countable_Set.thy	Mon Sep 03 13:32:29 2018 +0100
     5.3 @@ -69,6 +69,11 @@
     5.4    then show thesis ..
     5.5  qed
     5.6  
     5.7 +lemma countable_infiniteE':
     5.8 +  assumes "countable A" "infinite A"
     5.9 +  obtains g where "bij_betw g (UNIV :: nat set) A"
    5.10 +  using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
    5.11 +
    5.12  lemma countable_enum_cases:
    5.13    assumes "countable S"
    5.14    obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
     6.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Mon Sep 03 13:28:52 2018 +0100
     6.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Mon Sep 03 13:32:29 2018 +0100
     6.3 @@ -71,6 +71,11 @@
     6.4    shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
     6.5    by (rule antisym) (auto intro!: INF_greatest INF_lower2)
     6.6  
     6.7 +lemma INF_Sigma:
     6.8 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
     6.9 +  shows "(INF i : A. INF j : B i. f i j) = (INF p : Sigma A B. f (fst p) (snd p))"
    6.10 +  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    6.11 +
    6.12  subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
    6.13  
    6.14  definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    6.15 @@ -202,7 +207,7 @@
    6.16  lemma le_Limsup:
    6.17    assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
    6.18    shows "l \<le> Limsup F f"
    6.19 -  using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
    6.20 +  using F Liminf_bounded[of l f F] Liminf_le_Limsup[of F f] order.trans x by blast
    6.21  
    6.22  lemma Liminf_le:
    6.23    assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
     7.1 --- a/src/HOL/Limits.thy	Mon Sep 03 13:28:52 2018 +0100
     7.2 +++ b/src/HOL/Limits.thy	Mon Sep 03 13:32:29 2018 +0100
     7.3 @@ -876,6 +876,91 @@
     7.4      and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
     7.5  
     7.6  
     7.7 +class topological_monoid_mult = topological_semigroup_mult + monoid_mult
     7.8 +class topological_comm_monoid_mult = topological_monoid_mult + comm_monoid_mult
     7.9 +
    7.10 +lemma tendsto_power_strong [tendsto_intros]:
    7.11 +  fixes f :: "_ \<Rightarrow> 'b :: topological_monoid_mult"
    7.12 +  assumes "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
    7.13 +  shows   "((\<lambda>x. f x ^ g x) \<longlongrightarrow> a ^ b) F"
    7.14 +proof -
    7.15 +  have "((\<lambda>x. f x ^ b) \<longlongrightarrow> a ^ b) F"
    7.16 +    by (induction b) (auto intro: tendsto_intros assms)
    7.17 +  also from assms(2) have "eventually (\<lambda>x. g x = b) F"
    7.18 +    by (simp add: nhds_discrete filterlim_principal)
    7.19 +  hence "eventually (\<lambda>x. f x ^ b = f x ^ g x) F"
    7.20 +    by eventually_elim simp
    7.21 +  hence "((\<lambda>x. f x ^ b) \<longlongrightarrow> a ^ b) F \<longleftrightarrow> ((\<lambda>x. f x ^ g x) \<longlongrightarrow> a ^ b) F"
    7.22 +    by (intro filterlim_cong refl)
    7.23 +  finally show ?thesis .
    7.24 +qed
    7.25 +
    7.26 +lemma continuous_mult' [continuous_intros]:
    7.27 +  fixes f g :: "_ \<Rightarrow> 'b::topological_semigroup_mult"
    7.28 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
    7.29 +  unfolding continuous_def by (rule tendsto_mult)
    7.30 +
    7.31 +lemma continuous_power' [continuous_intros]:
    7.32 +  fixes f :: "_ \<Rightarrow> 'b::topological_monoid_mult"
    7.33 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ^ g x)"
    7.34 +  unfolding continuous_def by (rule tendsto_power_strong) auto
    7.35 +
    7.36 +lemma continuous_on_mult' [continuous_intros]:
    7.37 +  fixes f g :: "_ \<Rightarrow> 'b::topological_semigroup_mult"
    7.38 +  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x * g x)"
    7.39 +  unfolding continuous_on_def by (auto intro: tendsto_mult)
    7.40 +
    7.41 +lemma continuous_on_power' [continuous_intros]:
    7.42 +  fixes f :: "_ \<Rightarrow> 'b::topological_monoid_mult"
    7.43 +  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x ^ g x)"
    7.44 +  unfolding continuous_on_def by (auto intro: tendsto_power_strong)
    7.45 +
    7.46 +lemma tendsto_mult_one:
    7.47 +  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_mult"
    7.48 +  shows "(f \<longlongrightarrow> 1) F \<Longrightarrow> (g \<longlongrightarrow> 1) F \<Longrightarrow> ((\<lambda>x. f x * g x) \<longlongrightarrow> 1) F"
    7.49 +  by (drule (1) tendsto_mult) simp
    7.50 +
    7.51 +lemma tendsto_prod' [tendsto_intros]:
    7.52 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_mult"
    7.53 +  shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>I. f i x) \<longlongrightarrow> (\<Prod>i\<in>I. a i)) F"
    7.54 +  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_mult)
    7.55 +
    7.56 +lemma tendsto_one_prod':
    7.57 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_mult"
    7.58 +  assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 1) F"
    7.59 +  shows "((\<lambda>i. prod (f i) I) \<longlongrightarrow> 1) F"
    7.60 +  using tendsto_prod' [of I "\<lambda>x y. f y x" "\<lambda>x. 1"] assms by simp
    7.61 +
    7.62 +lemma continuous_prod' [continuous_intros]:
    7.63 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_mult"
    7.64 +  shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>I. f i x)"
    7.65 +  unfolding continuous_def by (rule tendsto_prod')
    7.66 +
    7.67 +lemma continuous_on_prod' [continuous_intros]:
    7.68 +  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_mult"
    7.69 +  shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Prod>i\<in>I. f i x)"
    7.70 +  unfolding continuous_on_def by (auto intro: tendsto_prod')
    7.71 +
    7.72 +instance nat :: topological_comm_monoid_mult
    7.73 +  by standard
    7.74 +    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
    7.75 +
    7.76 +instance int :: topological_comm_monoid_mult
    7.77 +  by standard
    7.78 +    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
    7.79 +
    7.80 +class comm_real_normed_algebra_1 = real_normed_algebra_1 + comm_monoid_mult
    7.81 +
    7.82 +context real_normed_field
    7.83 +begin
    7.84 +
    7.85 +subclass comm_real_normed_algebra_1
    7.86 +proof
    7.87 +  from norm_mult[of "1 :: 'a" 1] show "norm 1 = 1" by simp 
    7.88 +qed (simp_all add: norm_mult)
    7.89 +
    7.90 +end
    7.91 +
    7.92  subsubsection \<open>Inverse and division\<close>
    7.93  
    7.94  lemma (in bounded_bilinear) Zfun_prod_Bfun:
     8.1 --- a/src/HOL/Series.thy	Mon Sep 03 13:28:52 2018 +0100
     8.2 +++ b/src/HOL/Series.thy	Mon Sep 03 13:32:29 2018 +0100
     8.3 @@ -335,6 +335,18 @@
     8.4  
     8.5  end
     8.6  
     8.7 +lemma sums_If_finite_set':
     8.8 +  fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_ab_group_add}"
     8.9 +  assumes "g sums S" and "finite A" and "S' = S + (\<Sum>n\<in>A. f n - g n)"
    8.10 +  shows   "(\<lambda>n. if n \<in> A then f n else g n) sums S'"
    8.11 +proof -
    8.12 +  have "(\<lambda>n. g n + (if n \<in> A then f n - g n else 0)) sums (S + (\<Sum>n\<in>A. f n - g n))"
    8.13 +    by (intro sums_add assms sums_If_finite_set)
    8.14 +  also have "(\<lambda>n. g n + (if n \<in> A then f n - g n else 0)) = (\<lambda>n. if n \<in> A then f n else g n)"
    8.15 +    by (simp add: fun_eq_iff)
    8.16 +  finally show ?thesis using assms by simp
    8.17 +qed
    8.18 +
    8.19  subsection \<open>Infinite summability on real normed vector spaces\<close>
    8.20  
    8.21  context
     9.1 --- a/src/HOL/Tools/ATP/scripts/remote_atp	Mon Sep 03 13:28:52 2018 +0100
     9.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp	Mon Sep 03 13:32:29 2018 +0100
     9.3 @@ -12,7 +12,7 @@
     9.4  use LWP;
     9.5  
     9.6  my $SystemOnTPTPFormReplyURL =
     9.7 -  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
     9.8 +  "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply";
     9.9  
    9.10  # default parameters
    9.11  my %URLParameters = (
    10.1 --- a/src/HOL/Topological_Spaces.thy	Mon Sep 03 13:28:52 2018 +0100
    10.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Sep 03 13:32:29 2018 +0100
    10.3 @@ -512,6 +512,10 @@
    10.4  lemma (in discrete_topology) at_discrete: "at x within S = bot"
    10.5    unfolding at_within_def nhds_discrete by simp
    10.6  
    10.7 +lemma (in discrete_topology) tendsto_discrete:
    10.8 +  "filterlim (f :: 'b \<Rightarrow> 'a) (nhds y) F \<longleftrightarrow> eventually (\<lambda>x. f x = y) F"
    10.9 +  by (auto simp: nhds_discrete filterlim_principal)
   10.10 +
   10.11  lemma (in topological_space) at_within_eq:
   10.12    "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
   10.13    unfolding nhds_def at_within_def
   10.14 @@ -881,6 +885,36 @@
   10.15    shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
   10.16    by (auto intro!: tendsto_unique [OF assms tendsto_const])
   10.17  
   10.18 +lemma Lim_in_closed_set:
   10.19 +  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) F" "F \<noteq> bot" "(f \<longlongrightarrow> l) F"
   10.20 +  shows "l \<in> S"
   10.21 +proof (rule ccontr)
   10.22 +  assume "l \<notin> S"
   10.23 +  with \<open>closed S\<close> have "open (- S)" "l \<in> - S"
   10.24 +    by (simp_all add: open_Compl)
   10.25 +  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) F"
   10.26 +    by (rule topological_tendstoD)
   10.27 +  with assms(2) have "eventually (\<lambda>x. False) F"
   10.28 +    by (rule eventually_elim2) simp
   10.29 +  with assms(3) show "False"
   10.30 +    by (simp add: eventually_False)
   10.31 +qed
   10.32 +
   10.33 +lemma (in t3_space) nhds_closed:
   10.34 +  assumes "x \<in> A" and "open A"
   10.35 +  shows   "\<exists>A'. x \<in> A' \<and> closed A' \<and> A' \<subseteq> A \<and> eventually (\<lambda>y. y \<in> A') (nhds x)"
   10.36 +proof -
   10.37 +  from assms have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> - A \<subseteq> V \<and> U \<inter> V = {}"
   10.38 +    by (intro t3_space) auto
   10.39 +  then obtain U V where UV: "open U" "open V" "x \<in> U" "-A \<subseteq> V" "U \<inter> V = {}"
   10.40 +    by auto
   10.41 +  have "eventually (\<lambda>y. y \<in> U) (nhds x)"
   10.42 +    using \<open>open U\<close> and \<open>x \<in> U\<close> by (intro eventually_nhds_in_open)
   10.43 +  hence "eventually (\<lambda>y. y \<in> -V) (nhds x)"
   10.44 +    by eventually_elim (use UV in auto)
   10.45 +  with UV show ?thesis by (intro exI[of _ "-V"]) auto
   10.46 +qed
   10.47 +
   10.48  lemma (in order_topology) increasing_tendsto:
   10.49    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
   10.50      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   10.51 @@ -2082,6 +2116,9 @@
   10.52    by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
   10.53        dest: bspec[where x=a] bspec[where x=b])
   10.54  
   10.55 +lemma continuous_on_discrete [simp, continuous_intros]:
   10.56 +  "continuous_on A (f :: 'a :: discrete_topology \<Rightarrow> _)"
   10.57 +  by (auto simp: continuous_on_def at_discrete)
   10.58  
   10.59  subsubsection \<open>Continuity at a point\<close>
   10.60  
   10.61 @@ -2125,6 +2162,10 @@
   10.62    "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. continuous (at x within s) f)"
   10.63    unfolding continuous_on_def continuous_within ..
   10.64  
   10.65 +lemma continuous_discrete [simp, continuous_intros]:
   10.66 +  "continuous (at x within A) (f :: 'a :: discrete_topology \<Rightarrow> _)"
   10.67 +  by (auto simp: continuous_def at_discrete)
   10.68 +
   10.69  abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool"
   10.70    where "isCont f a \<equiv> continuous (at a) f"
   10.71  
    11.1 --- a/src/Pure/Concurrent/lazy.ML	Mon Sep 03 13:28:52 2018 +0100
    11.2 +++ b/src/Pure/Concurrent/lazy.ML	Mon Sep 03 13:32:29 2018 +0100
    11.3 @@ -15,7 +15,8 @@
    11.4    val peek: 'a lazy -> 'a Exn.result option
    11.5    val is_running: 'a lazy -> bool
    11.6    val is_finished: 'a lazy -> bool
    11.7 -  val force_result: 'a lazy -> 'a Exn.result
    11.8 +  val finished_result: 'a lazy -> 'a Exn.result
    11.9 +  val force_result: {strict: bool} -> 'a lazy -> 'a Exn.result
   11.10    val force: 'a lazy -> 'a
   11.11    val force_value: 'a lazy -> 'a lazy
   11.12    val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   11.13 @@ -59,18 +60,28 @@
   11.14          Expr _ => false
   11.15        | Result res => not (Future.is_finished res));
   11.16  
   11.17 +fun is_finished_future res =
   11.18 +  Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res));
   11.19 +
   11.20  fun is_finished (Value _) = true
   11.21    | is_finished (Lazy var) =
   11.22        (case Synchronized.value var of
   11.23          Expr _ => false
   11.24 -      | Result res =>
   11.25 -          Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
   11.26 +      | Result res => is_finished_future res);
   11.27 +
   11.28 +fun finished_result (Value a) = Exn.Res a
   11.29 +  | finished_result (Lazy var) =
   11.30 +      let fun fail () = Exn.Exn (Fail "Unfinished lazy") in
   11.31 +        (case Synchronized.value var of
   11.32 +          Expr _ => fail ()
   11.33 +        | Result res => if is_finished_future res then Future.join_result res else fail ())
   11.34 +      end;
   11.35  
   11.36  
   11.37  (* force result *)
   11.38  
   11.39 -fun force_result (Value a) = Exn.Res a
   11.40 -  | force_result (Lazy var) =
   11.41 +fun force_result _ (Value a) = Exn.Res a
   11.42 +  | force_result {strict} (Lazy var) =
   11.43        (case peek (Lazy var) of
   11.44          SOME res => res
   11.45        | NONE =>
   11.46 @@ -93,19 +104,22 @@
   11.47                      val res0 = Exn.capture (restore_attributes e) ();
   11.48                      val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
   11.49                      val res = Future.join_result x;
   11.50 -                    (*semantic race: some other threads might see the same
   11.51 -                      interrupt, until there is a fresh start*)
   11.52                      val _ =
   11.53 -                      if Exn.is_interrupt_exn res
   11.54 -                      then Synchronized.change var (fn _ => Expr (name, e))
   11.55 -                      else Synchronized.assign var (Result (Future.value_result res));
   11.56 +                      if not (Exn.is_interrupt_exn res) then
   11.57 +                        Synchronized.assign var (Result (Future.value_result res))
   11.58 +                      else if strict then
   11.59 +                        Synchronized.assign var
   11.60 +                          (Result (Future.value_result (Exn.Exn (Fail "Interrupt"))))
   11.61 +                      (*semantic race: some other threads might see the same
   11.62 +                        interrupt, until there is a fresh start*)
   11.63 +                      else Synchronized.change var (fn _ => Expr (name, e));
   11.64                    in res end
   11.65                | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
   11.66              end) ());
   11.67  
   11.68  end;
   11.69  
   11.70 -fun force x = Exn.release (force_result x);
   11.71 +fun force x = Exn.release (force_result {strict = false} x);
   11.72  
   11.73  fun force_value x = if is_value x then x else value (force x);
   11.74  
   11.75 @@ -122,7 +136,8 @@
   11.76  fun consolidate xs =
   11.77    let
   11.78      val unfinished =
   11.79 -      xs |> map_filter (fn x => if is_finished x then NONE else SOME (fn () => force_result x));
   11.80 +      xs |> map_filter (fn x =>
   11.81 +        if is_finished x then NONE else SOME (fn () => force_result {strict = false} x));
   11.82      val _ =
   11.83        if Future.relevant unfinished then
   11.84          ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} unfinished)
   11.85 @@ -133,7 +148,7 @@
   11.86  (* future evaluation *)
   11.87  
   11.88  fun future params x =
   11.89 -  if is_finished x then Future.value_result (force_result x)
   11.90 +  if is_finished x then Future.value_result (force_result {strict = false} x)
   11.91    else (singleton o Future.forks) params (fn () => force x);
   11.92  
   11.93  
    12.1 --- a/src/Pure/General/position.ML	Mon Sep 03 13:28:52 2018 +0100
    12.2 +++ b/src/Pure/General/position.ML	Mon Sep 03 13:32:29 2018 +0100
    12.3 @@ -29,6 +29,7 @@
    12.4    val id_only: string -> T
    12.5    val get_id: T -> string option
    12.6    val put_id: string -> T -> T
    12.7 +  val copy_id: T -> T -> T
    12.8    val id_properties_of: T -> Properties.T
    12.9    val parse_id: T -> int option
   12.10    val adjust_offsets: (int -> int option) -> T -> T
   12.11 @@ -142,6 +143,7 @@
   12.12  
   12.13  fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   12.14  fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
   12.15 +fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
   12.16  
   12.17  fun parse_id pos = Option.map Value.parse_int (get_id pos);
   12.18  
   12.19 @@ -151,14 +153,16 @@
   12.20    | NONE => []);
   12.21  
   12.22  fun adjust_offsets adjust (pos as Pos (_, props)) =
   12.23 -  (case parse_id pos of
   12.24 -    SOME id =>
   12.25 -      (case adjust id of
   12.26 -        SOME offset =>
   12.27 -          let val Pos (count, _) = advance_offsets offset pos
   12.28 -          in Pos (count, Properties.remove Markup.idN props) end
   12.29 -      | NONE => pos)
   12.30 -  | NONE => pos);
   12.31 +  if is_none (file_of pos) then
   12.32 +    (case parse_id pos of
   12.33 +      SOME id =>
   12.34 +        (case adjust id of
   12.35 +          SOME offset =>
   12.36 +            let val Pos (count, _) = advance_offsets offset pos
   12.37 +            in Pos (count, Properties.remove Markup.idN props) end
   12.38 +        | NONE => pos)
   12.39 +    | NONE => pos)
   12.40 +  else pos;
   12.41  
   12.42  
   12.43  (* markup properties *)
    13.1 --- a/src/Pure/Isar/class.ML	Mon Sep 03 13:28:52 2018 +0100
    13.2 +++ b/src/Pure/Isar/class.ML	Mon Sep 03 13:32:29 2018 +0100
    13.3 @@ -229,9 +229,13 @@
    13.4  
    13.5  fun activate_defs class thms thy =
    13.6    (case Element.eq_morphism thy thms of
    13.7 -    SOME eq_morph => fold (fn cls => fn thy =>
    13.8 -      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
    13.9 -        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   13.10 +    SOME eq_morph =>
   13.11 +      fold (fn cls => fn thy =>
   13.12 +        Context.theory_map
   13.13 +          (Locale.amend_registration
   13.14 +            {dep = (cls, base_morphism thy cls),
   13.15 +              mixin = SOME (eq_morph, true),
   13.16 +              export = export_morphism thy cls}) thy) (heritage thy [class]) thy
   13.17    | NONE => thy);
   13.18  
   13.19  fun register_operation class (c, t) input_only thy =
   13.20 @@ -484,10 +488,13 @@
   13.21      val diff_sort = Sign.complete_sort thy [sup]
   13.22        |> subtract (op =) (Sign.complete_sort thy [sub])
   13.23        |> filter (is_class thy);
   13.24 -    fun add_dependency some_wit = case some_dep_morph of
   13.25 -        SOME dep_morph => Generic_Target.locale_dependency sub
   13.26 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export
   13.27 -      | NONE => I;
   13.28 +    fun add_dependency some_wit (* FIXME unused!? *) =
   13.29 +      (case some_dep_morph of
   13.30 +        SOME dep_morph =>
   13.31 +          Generic_Target.locale_dependency sub
   13.32 +            {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
   13.33 +              mixin = NONE, export = export}
   13.34 +      | NONE => I);
   13.35    in
   13.36      lthy
   13.37      |> Local_Theory.raw_theory
    14.1 --- a/src/Pure/Isar/class_declaration.ML	Mon Sep 03 13:28:52 2018 +0100
    14.2 +++ b/src/Pure/Isar/class_declaration.ML	Mon Sep 03 13:32:29 2018 +0100
    14.3 @@ -328,8 +328,10 @@
    14.4      |-> (fn (param_map, params, assm_axiom) =>
    14.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    14.6      #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
    14.7 -       Context.theory_map (Locale.add_registration (class, base_morph)
    14.8 -         (Option.map (rpair true) eq_morph) export_morph)
    14.9 +       Locale.add_registration_theory
   14.10 +         {dep = (class, base_morph),
   14.11 +           mixin = Option.map (rpair true) eq_morph,
   14.12 +           export = export_morph}
   14.13      #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
   14.14      #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
   14.15      |> snd
    15.1 --- a/src/Pure/Isar/expression.ML	Mon Sep 03 13:28:52 2018 +0100
    15.2 +++ b/src/Pure/Isar/expression.ML	Mon Sep 03 13:32:29 2018 +0100
    15.3 @@ -531,12 +531,8 @@
    15.4  local
    15.5  
    15.6  fun props_of thy (name, morph) =
    15.7 -  let
    15.8 -    val (asm, defs) = Locale.specification_of thy name;
    15.9 -  in
   15.10 -    (case asm of NONE => defs | SOME asm => asm :: defs)
   15.11 -    |> map (Morphism.term morph)
   15.12 -  end;
   15.13 +  let val (asm, defs) = Locale.specification_of thy name
   15.14 +  in map (Morphism.term morph) (the_list asm @ defs) end;
   15.15  
   15.16  fun prep_goal_expression prep expression ctxt =
   15.17    let
    16.1 --- a/src/Pure/Isar/generic_target.ML	Mon Sep 03 13:28:52 2018 +0100
    16.2 +++ b/src/Pure/Isar/generic_target.ML	Mon Sep 03 13:32:29 2018 +0100
    16.3 @@ -52,8 +52,7 @@
    16.4    val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
    16.5      local_theory -> (term * term) * local_theory
    16.6    val theory_declaration: declaration -> local_theory -> local_theory
    16.7 -  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    16.8 -    local_theory -> local_theory
    16.9 +  val theory_registration: Locale.registration -> local_theory -> local_theory
   16.10  
   16.11    (*locale target primitives*)
   16.12    val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
   16.13 @@ -71,8 +70,7 @@
   16.14      local_theory -> local_theory
   16.15    val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
   16.16      local_theory -> local_theory
   16.17 -  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
   16.18 -    local_theory -> local_theory
   16.19 +  val locale_dependency: string -> Locale.registration -> local_theory -> local_theory
   16.20  
   16.21    (*initialisation*)
   16.22    val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
   16.23 @@ -372,7 +370,7 @@
   16.24    background_declaration decl #> standard_declaration (K true) decl;
   16.25  
   16.26  val theory_registration =
   16.27 -  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
   16.28 +  Local_Theory.raw_theory o Locale.add_registration_theory;
   16.29  
   16.30  
   16.31  
   16.32 @@ -406,9 +404,9 @@
   16.33    locale_target_const locale (K true) prmode ((b, mx), rhs)
   16.34    #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
   16.35  
   16.36 -fun locale_dependency locale dep_morph mixin export =
   16.37 -  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
   16.38 -  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
   16.39 +fun locale_dependency locale registration =
   16.40 +  Local_Theory.raw_theory (Locale.add_dependency locale registration)
   16.41 +  #> Locale.add_registration_local_theory registration;
   16.42  
   16.43  
   16.44  (** locale abbreviations **)
    17.1 --- a/src/Pure/Isar/interpretation.ML	Mon Sep 03 13:28:52 2018 +0100
    17.2 +++ b/src/Pure/Isar/interpretation.ML	Mon Sep 03 13:32:29 2018 +0100
    17.3 @@ -97,30 +97,30 @@
    17.4  
    17.5  local
    17.6  
    17.7 -fun meta_rewrite eqns ctxt =
    17.8 +fun abs_def_rule eqns ctxt =
    17.9    (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
   17.10  
   17.11 -fun note_eqns_register pos note activate deps eqnss witss def_eqns thms export export' ctxt =
   17.12 +fun note_eqns_register note add_registration
   17.13 +    deps eqnss witss def_eqns thms export export' ctxt =
   17.14    let
   17.15 -    val thmss = unflat ((map o map) fst eqnss) thms;
   17.16 -    val factss =
   17.17 -      map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss;
   17.18 -    val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
   17.19 +    val factss = thms
   17.20 +      |> unflat ((map o map) #1 eqnss)
   17.21 +      |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
   17.22 +    val (eqnss', ctxt') =
   17.23 +      fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
   17.24      val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
   17.25 -    val (eqns', ctxt'') = ctxt'
   17.26 -      |> note Thm.theoremK [defs]
   17.27 -      |-> meta_rewrite;
   17.28 -    val dep_morphs =
   17.29 -      map2 (fn (dep, morph) => fn wits =>
   17.30 -        let val morph' = morph
   17.31 -          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
   17.32 -          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
   17.33 -        in (dep, morph') end) deps witss;
   17.34 -    fun activate' (dep_morph, eqns) ctxt =
   17.35 -      activate dep_morph
   17.36 -        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
   17.37 -        export ctxt;
   17.38 -  in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end;
   17.39 +    val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
   17.40 +    val deps' =
   17.41 +      (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
   17.42 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
   17.43 +    fun register (dep, eqns) ctxt =
   17.44 +      ctxt |> add_registration
   17.45 +        {dep = dep,
   17.46 +          mixin =
   17.47 +            Option.map (rpair true)
   17.48 +              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
   17.49 +          export = export};
   17.50 +  in ctxt'' |> fold register (deps' ~~ eqnss') end;
   17.51  
   17.52  in
   17.53  
   17.54 @@ -129,9 +129,8 @@
   17.55    let
   17.56      val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
   17.57        prep_interpretation expression raw_defs initial_ctxt;
   17.58 -    val pos = Position.thread_data ();
   17.59      fun after_qed witss eqns =
   17.60 -      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
   17.61 +      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
   17.62    in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
   17.63  
   17.64  end;
   17.65 @@ -143,23 +142,16 @@
   17.66  
   17.67  local
   17.68  
   17.69 +fun setup_proof state after_qed propss eqns goal_ctxt =
   17.70 +  Element.witness_local_proof_eqs
   17.71 +    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
   17.72 +    "interpret" propss eqns goal_ctxt state;
   17.73 +
   17.74  fun gen_interpret prep_interpretation expression state =
   17.75 -  let
   17.76 -    val _ = Proof.assert_forward_or_chain state;
   17.77 -    fun lift_after_qed after_qed witss eqns =
   17.78 -      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
   17.79 -    fun setup_proof after_qed propss eqns goal_ctxt =
   17.80 -      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
   17.81 -        propss eqns goal_ctxt state;
   17.82 -    fun add_registration reg mixin export ctxt = ctxt
   17.83 -      |> Proof_Context.set_stmt false
   17.84 -      |> Context.proof_map (Locale.add_registration reg mixin export)
   17.85 -      |> Proof_Context.restore_stmt ctxt;
   17.86 -  in
   17.87 -    Proof.context_of state
   17.88 -    |> generic_interpretation prep_interpretation setup_proof
   17.89 -      Attrib.local_notes add_registration expression []
   17.90 -  end;
   17.91 +  Proof.assert_forward_or_chain state
   17.92 +  |> Proof.context_of
   17.93 +  |> generic_interpretation prep_interpretation (setup_proof state)
   17.94 +    Attrib.local_notes Locale.add_registration_proof expression [];
   17.95  
   17.96  in
   17.97  
    18.1 --- a/src/Pure/Isar/local_theory.ML	Mon Sep 03 13:28:52 2018 +0100
    18.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Sep 03 13:32:29 2018 +0100
    18.3 @@ -14,6 +14,11 @@
    18.4    type fact = binding * thms;
    18.5  end;
    18.6  
    18.7 +structure Locale =
    18.8 +struct
    18.9 +  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism};
   18.10 +end;
   18.11 +
   18.12  signature LOCAL_THEORY =
   18.13  sig
   18.14    type operations
   18.15 @@ -54,10 +59,8 @@
   18.16    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   18.17      (term * term) * local_theory
   18.18    val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
   18.19 -  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
   18.20 -    local_theory -> local_theory
   18.21 -  val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
   18.22 -    local_theory -> local_theory
   18.23 +  val theory_registration: Locale.registration -> local_theory -> local_theory
   18.24 +  val locale_dependency: Locale.registration -> local_theory -> local_theory
   18.25    val pretty: local_theory -> Pretty.T list
   18.26    val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   18.27    val set_defsort: sort -> local_theory -> local_theory
   18.28 @@ -91,10 +94,8 @@
   18.29    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   18.30      (term * term) * local_theory,
   18.31    declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
   18.32 -  theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
   18.33 -     local_theory -> local_theory,
   18.34 -  locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
   18.35 -     local_theory -> local_theory,
   18.36 +  theory_registration: Locale.registration -> local_theory -> local_theory,
   18.37 +  locale_dependency: Locale.registration -> local_theory -> local_theory,
   18.38    pretty: local_theory -> Pretty.T list};
   18.39  
   18.40  type lthy =
   18.41 @@ -250,7 +251,7 @@
   18.42  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
   18.43  
   18.44  fun propagate_ml_env (context as Context.Proof lthy) =
   18.45 -      let val inherit = ML_Env.inherit context in
   18.46 +      let val inherit = ML_Env.inherit [context] in
   18.47          lthy
   18.48          |> background_theory (Context.theory_map inherit)
   18.49          |> map_contexts (K (Context.proof_map inherit))
   18.50 @@ -276,10 +277,10 @@
   18.51  val define_internal = operation2 #define true;
   18.52  val notes_kind = operation2 #notes;
   18.53  val declaration = operation2 #declaration;
   18.54 -fun theory_registration dep_morph mixin export =
   18.55 -  assert_bottom #> operation (fn ops => #theory_registration ops dep_morph mixin export);
   18.56 -fun locale_dependency dep_morph mixin export =
   18.57 -  assert_bottom #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
   18.58 +fun theory_registration registration =
   18.59 +  assert_bottom #> operation (fn ops => #theory_registration ops registration);
   18.60 +fun locale_dependency registration =
   18.61 +  assert_bottom #> operation (fn ops => #locale_dependency ops registration);
   18.62  
   18.63  
   18.64  (* theorems *)
    19.1 --- a/src/Pure/Isar/locale.ML	Mon Sep 03 13:28:52 2018 +0100
    19.2 +++ b/src/Pure/Isar/locale.ML	Mon Sep 03 13:32:29 2018 +0100
    19.3 @@ -42,6 +42,7 @@
    19.4      declaration list ->
    19.5      (string * Attrib.fact list) list ->
    19.6      (string * morphism) list -> theory -> theory
    19.7 +  val locale_space: theory -> Name_Space.T
    19.8    val intern: theory -> xstring -> string
    19.9    val check: theory -> xstring * Position.T -> string
   19.10    val extern: theory -> string -> xstring
   19.11 @@ -53,6 +54,14 @@
   19.12    val axioms_of: theory -> string -> thm list
   19.13    val instance_of: theory -> string -> morphism -> term list
   19.14    val specification_of: theory -> string -> term option * term list
   19.15 +  val hyp_spec_of: theory -> string -> Element.context_i list
   19.16 +
   19.17 +  type content =
   19.18 +   {type_params: (string * sort) list,
   19.19 +    params: ((string * typ) * mixfix) list,
   19.20 +    asm: term option,
   19.21 +    defs: term list}
   19.22 +  val dest_locales: theory -> (string * content) list
   19.23  
   19.24    (* Storing results *)
   19.25    val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
   19.26 @@ -73,20 +82,17 @@
   19.27    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
   19.28  
   19.29    (* Registrations and dependencies *)
   19.30 -  val add_registration: string * morphism -> (morphism * bool) option ->
   19.31 -    morphism -> Context.generic -> Context.generic
   19.32 -  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
   19.33 -    local_theory -> local_theory
   19.34 -  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
   19.35 -    local_theory -> local_theory
   19.36 -  val amend_registration: string * morphism -> morphism * bool ->
   19.37 -    morphism -> Context.generic -> Context.generic
   19.38 +  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
   19.39 +  val amend_registration: registration -> Context.generic -> Context.generic
   19.40 +  val add_registration: registration -> Context.generic -> Context.generic
   19.41 +  val add_registration_theory: registration -> theory -> theory
   19.42 +  val add_registration_proof: registration -> Proof.context -> Proof.context
   19.43 +  val add_registration_local_theory: registration -> local_theory -> local_theory
   19.44 +  val activate_fragment: registration -> local_theory -> local_theory
   19.45    val registrations_of: Context.generic -> string -> (string * morphism) list
   19.46 -  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
   19.47 -    morphism -> theory -> theory
   19.48 +  val add_dependency: string -> registration -> theory -> theory
   19.49  
   19.50    (* Diagnostic *)
   19.51 -  val hyp_spec_of: theory -> string -> Element.context_i list
   19.52    val print_locales: bool -> theory -> unit
   19.53    val print_locale: theory -> bool -> xstring * Position.T -> unit
   19.54    val print_registrations: Proof.context -> xstring * Position.T -> unit
   19.55 @@ -209,6 +215,20 @@
   19.56    Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
   19.57  
   19.58  
   19.59 +(* content *)
   19.60 +
   19.61 +type content =
   19.62 + {type_params: (string * sort) list,
   19.63 +  params: ((string * typ) * mixfix) list,
   19.64 +  asm: term option,
   19.65 +  defs: term list};
   19.66 +
   19.67 +fun dest_locales thy =
   19.68 +  (Locales.get thy, []) |-> Name_Space.fold_table
   19.69 +    (fn (name, Loc {parameters = (type_params, params), spec = (asm, defs), ...}) =>
   19.70 +      cons (name, {type_params = type_params, params = params, asm = asm, defs = defs}));
   19.71 +
   19.72 +
   19.73  (** Primitive operations **)
   19.74  
   19.75  fun params_of thy = snd o #parameters o the_locale thy;
   19.76 @@ -222,8 +242,9 @@
   19.77  
   19.78  fun specification_of thy = #spec o the_locale thy;
   19.79  
   19.80 -fun dependencies_of thy name = the_locale thy name |>
   19.81 -  #dependencies;
   19.82 +fun hyp_spec_of thy = #hyp_spec o the_locale thy;
   19.83 +
   19.84 +fun dependencies_of thy = #dependencies o the_locale thy;
   19.85  
   19.86  fun mixins_of thy name serial = the_locale thy name |>
   19.87    #mixins |> lookup_mixins serial;
   19.88 @@ -516,60 +537,68 @@
   19.89  
   19.90  (*** Add and extend registrations ***)
   19.91  
   19.92 -fun amend_registration (name, morph) mixin export context =
   19.93 -  let
   19.94 -    val thy = Context.theory_of context;
   19.95 -    val ctxt = Context.proof_of context;
   19.96 +type registration = Locale.registration;
   19.97 +
   19.98 +fun amend_registration {mixin = NONE, ...} context = context
   19.99 +  | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
  19.100 +      let
  19.101 +        val thy = Context.theory_of context;
  19.102 +        val ctxt = Context.proof_of context;
  19.103  
  19.104 -    val regs = Registrations.get context |> fst;
  19.105 -    val base = instance_of thy name (morph $> export);
  19.106 -    val serial' =
  19.107 -      (case Idtab.lookup regs (name, base) of
  19.108 -        NONE =>
  19.109 -          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
  19.110 -            " with\nparameter instantiation " ^
  19.111 -            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
  19.112 -            " available")
  19.113 -      | SOME (_, serial') => serial');
  19.114 -  in
  19.115 -    add_mixin serial' mixin context
  19.116 -  end;
  19.117 +        val regs = Registrations.get context |> fst;
  19.118 +        val base = instance_of thy name (morph $> export);
  19.119 +        val serial' =
  19.120 +          (case Idtab.lookup regs (name, base) of
  19.121 +            NONE =>
  19.122 +              error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
  19.123 +                " with\nparameter instantiation " ^
  19.124 +                space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
  19.125 +                " available")
  19.126 +          | SOME (_, serial') => serial');
  19.127 +      in
  19.128 +        add_mixin serial' mixin context
  19.129 +      end;
  19.130  
  19.131  (* Note that a registration that would be subsumed by an existing one will not be
  19.132     generated, and it will not be possible to amend it. *)
  19.133  
  19.134 -fun add_registration (name, base_morph) mixin export context =
  19.135 +fun add_registration {dep = (name, base_morph), mixin, export} context =
  19.136    let
  19.137      val thy = Context.theory_of context;
  19.138 -    val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
  19.139 -    val morph = base_morph $> mix;
  19.140 -    val inst = instance_of thy name morph;
  19.141 +    val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
  19.142 +    val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix);
  19.143 +    val inst = instance_of thy name mix_morph;
  19.144      val idents = Idents.get context;
  19.145    in
  19.146 -    if redundant_ident thy idents (name, inst)
  19.147 -    then context  (* FIXME amend mixins? *)
  19.148 +    if redundant_ident thy idents (name, inst) then context  (* FIXME amend mixins? *)
  19.149      else
  19.150        (idents, context)
  19.151        (* add new registrations with inherited mixins *)
  19.152 -      |> roundup thy (add_reg thy export) export (name, morph)
  19.153 -      |> snd
  19.154 +      |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2
  19.155        (* add mixin *)
  19.156 -      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
  19.157 +      |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export}
  19.158        (* activate import hierarchy as far as not already active *)
  19.159 -      |> activate_facts (SOME export) (name, morph)
  19.160 +      |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
  19.161 +  end;
  19.162 +
  19.163 +val add_registration_theory = Context.theory_map o add_registration;
  19.164 +
  19.165 +fun add_registration_proof registration ctxt = ctxt
  19.166 +  |> Proof_Context.set_stmt false
  19.167 +  |> Context.proof_map (add_registration registration)
  19.168 +  |> Proof_Context.restore_stmt ctxt;
  19.169 +
  19.170 +fun add_registration_local_theory registration lthy =
  19.171 +  let val n = Local_Theory.level lthy in
  19.172 +    lthy |> Local_Theory.map_contexts (fn level =>
  19.173 +      level = n - 1 ? Context.proof_map (add_registration registration))
  19.174    end;
  19.175  
  19.176  
  19.177  (* locale fragments within local theory *)
  19.178  
  19.179 -fun activate_fragment_nonbrittle dep_morph mixin export lthy =
  19.180 -  let val n = Local_Theory.level lthy in
  19.181 -    lthy |> Local_Theory.map_contexts (fn level =>
  19.182 -      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
  19.183 -  end;
  19.184 -
  19.185 -fun activate_fragment dep_morph mixin export =
  19.186 -  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
  19.187 +fun activate_fragment registration =
  19.188 +  Local_Theory.mark_brittle #> add_registration_local_theory registration;
  19.189  
  19.190  
  19.191  
  19.192 @@ -590,7 +619,7 @@
  19.193    end;
  19.194  *)
  19.195  
  19.196 -fun add_dependency loc (name, morph) mixin export thy =
  19.197 +fun add_dependency loc {dep = (name, morph), mixin, export} thy =
  19.198    let
  19.199      val serial' = serial ();
  19.200      val thy' = thy |>
  19.201 @@ -603,7 +632,7 @@
  19.202          (registrations_of context' loc) (Idents.get context', []);
  19.203    in
  19.204      thy'
  19.205 -    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
  19.206 +    |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs
  19.207    end;
  19.208  
  19.209  
  19.210 @@ -687,8 +716,6 @@
  19.211  
  19.212  (*** diagnostic commands and interfaces ***)
  19.213  
  19.214 -fun hyp_spec_of thy = #hyp_spec o the_locale thy;
  19.215 -
  19.216  fun print_locales verbose thy =
  19.217    Pretty.block
  19.218      (Pretty.breaks
    20.1 --- a/src/Pure/Isar/proof.ML	Mon Sep 03 13:28:52 2018 +0100
    20.2 +++ b/src/Pure/Isar/proof.ML	Mon Sep 03 13:32:29 2018 +0100
    20.3 @@ -33,7 +33,6 @@
    20.4    val enter_forward: state -> state
    20.5    val enter_chain: state -> state
    20.6    val enter_backward: state -> state
    20.7 -  val has_bottom_goal: state -> bool
    20.8    val using_facts: thm list -> state -> state
    20.9    val pretty_state: state -> Pretty.T list
   20.10    val refine: Method.text -> state -> state Seq.result Seq.seq
   20.11 @@ -95,6 +94,8 @@
   20.12    val end_block: state -> state
   20.13    val begin_notepad: context -> state
   20.14    val end_notepad: state -> context
   20.15 +  val is_notepad: state -> bool
   20.16 +  val reset_notepad: state -> state
   20.17    val proof: Method.text_range option -> state -> state Seq.result Seq.seq
   20.18    val defer: int -> state -> state
   20.19    val prefer: int -> state -> state
   20.20 @@ -237,7 +238,7 @@
   20.21  fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   20.22  
   20.23  fun propagate_ml_env state = map_contexts
   20.24 -  (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
   20.25 +  (Context.proof_map (ML_Env.inherit [Context.Proof (context_of state)])) state;
   20.26  
   20.27  
   20.28  (* facts *)
   20.29 @@ -326,17 +327,6 @@
   20.30  val before_qed = #before_qed o #2 o current_goal;
   20.31  
   20.32  
   20.33 -(* bottom goal *)
   20.34 -
   20.35 -fun has_bottom_goal (State stack) =
   20.36 -  let
   20.37 -    fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
   20.38 -      | bottom [Node {goal, ...}] = is_some goal
   20.39 -      | bottom [] = false
   20.40 -      | bottom (_ :: rest) = bottom rest;
   20.41 -  in bottom (op :: (Stack.dest stack)) end;
   20.42 -
   20.43 -
   20.44  (* nested goal *)
   20.45  
   20.46  fun map_goal f (State stack) =
   20.47 @@ -904,6 +894,20 @@
   20.48    #> close_block
   20.49    #> context_of;
   20.50  
   20.51 +fun get_notepad_context (State stack) =
   20.52 +  let
   20.53 +    fun escape [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = NONE
   20.54 +      | escape [Node {goal = SOME _, ...}] = NONE
   20.55 +      | escape [Node {goal = NONE, context = ctxt, ...}] = SOME ctxt
   20.56 +      | escape [] = NONE
   20.57 +      | escape (_ :: rest) = escape rest;
   20.58 +  in escape (op :: (Stack.dest stack)) end;
   20.59 +
   20.60 +val is_notepad = is_some o get_notepad_context;
   20.61 +
   20.62 +fun reset_notepad state =
   20.63 +  begin_notepad (the_default (context_of state) (get_notepad_context state));
   20.64 +
   20.65  
   20.66  (* sub-proofs *)
   20.67  
    21.1 --- a/src/Pure/Isar/toplevel.ML	Mon Sep 03 13:28:52 2018 +0100
    21.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Sep 03 13:32:29 2018 +0100
    21.3 @@ -65,7 +65,7 @@
    21.4      (local_theory -> Proof.state) -> transition -> transition
    21.5    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    21.6    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    21.7 -  val forget_proof: bool -> transition -> transition
    21.8 +  val forget_proof: transition -> transition
    21.9    val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   21.10    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   21.11    val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   21.12 @@ -84,6 +84,7 @@
   21.13    val command_exception: bool -> transition -> state -> state
   21.14    val reset_theory: state -> state option
   21.15    val reset_proof: state -> state option
   21.16 +  val reset_notepad: state -> state option
   21.17    type result
   21.18    val join_results: result -> (transition * state) list
   21.19    val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
   21.20 @@ -170,8 +171,7 @@
   21.21    | is_end_theory _ = false;
   21.22  
   21.23  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
   21.24 -  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
   21.25 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
   21.26 +  | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
   21.27  
   21.28  
   21.29  (* presentation context *)
   21.30 @@ -518,10 +518,10 @@
   21.31  
   21.32  end;
   21.33  
   21.34 -fun forget_proof strict = transaction (fn _ =>
   21.35 +val forget_proof = transaction (fn _ =>
   21.36    (fn Proof (prf, (_, orig_gthy)) =>
   21.37 -        if strict andalso not (Proof.has_bottom_goal (Proof_Node.current prf))
   21.38 -        then raise UNDEF else Theory (orig_gthy, NONE)
   21.39 +        if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF
   21.40 +        else Theory (orig_gthy, NONE)
   21.41      | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
   21.42      | _ => raise UNDEF));
   21.43  
   21.44 @@ -635,7 +635,7 @@
   21.45  
   21.46  in
   21.47  
   21.48 -val reset_theory = reset_state is_theory (forget_proof false);
   21.49 +val reset_theory = reset_state is_theory forget_proof;
   21.50  
   21.51  val reset_proof =
   21.52    reset_state is_proof
   21.53 @@ -643,6 +643,14 @@
   21.54        (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy))
   21.55          | _ => raise UNDEF)));
   21.56  
   21.57 +val reset_notepad =
   21.58 +  reset_state
   21.59 +    (fn st =>
   21.60 +      (case try proof_of st of
   21.61 +        SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state
   21.62 +      | NONE => true))
   21.63 +    (proof Proof.reset_notepad);
   21.64 +
   21.65  end;
   21.66  
   21.67  
    22.1 --- a/src/Pure/ML/ml_context.ML	Mon Sep 03 13:28:52 2018 +0100
    22.2 +++ b/src/Pure/ML/ml_context.ML	Mon Sep 03 13:32:29 2018 +0100
    22.3 @@ -168,7 +168,7 @@
    22.4          (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
    22.5          (fn () =>
    22.6            (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) ()
    22.7 -      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
    22.8 +      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit [context']));
    22.9  
   22.10      (*eval body*)
   22.11      val _ = ML_Compiler.eval flags pos body;
    23.1 --- a/src/Pure/ML/ml_env.ML	Mon Sep 03 13:28:52 2018 +0100
    23.2 +++ b/src/Pure/ML/ml_env.ML	Mon Sep 03 13:32:29 2018 +0100
    23.3 @@ -15,7 +15,7 @@
    23.4    val ML_read_global: bool Config.T
    23.5    val ML_write_global_raw: Config.raw
    23.6    val ML_write_global: bool Config.T
    23.7 -  val inherit: Context.generic -> Context.generic -> Context.generic
    23.8 +  val inherit: Context.generic list -> Context.generic -> Context.generic
    23.9    type operations =
   23.10     {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
   23.11      explode_token: ML_Lex.token -> char list}
   23.12 @@ -101,20 +101,31 @@
   23.13   {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
   23.14    explode_token: ML_Lex.token -> char list};
   23.15  
   23.16 +local
   23.17 +
   23.18  type env = tables * operations;
   23.19 +type data = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
   23.20 +
   23.21 +val empty_data: data = (Name_Space.empty_table "ML_environment", Inttab.empty);
   23.22 +
   23.23 +fun merge_data ((envs1, breakpoints1), (envs2, breakpoints2)) : data =
   23.24 +  ((envs1, envs2) |> Name_Space.join_tables
   23.25 +    (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
   23.26 +   Inttab.merge (K true) (breakpoints1, breakpoints2));
   23.27 +
   23.28 +in
   23.29  
   23.30  structure Data = Generic_Data
   23.31  (
   23.32 -  type T = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
   23.33 -  val empty: T = (Name_Space.empty_table "ML_environment", Inttab.empty);
   23.34 +  type T = data;
   23.35 +  val empty = empty_data;
   23.36    val extend = I;
   23.37 -  fun merge ((envs1, breakpoints1), (envs2, breakpoints2)) : T =
   23.38 -    ((envs1, envs2) |> Name_Space.join_tables
   23.39 -      (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
   23.40 -     Inttab.merge (K true) (breakpoints1, breakpoints2));
   23.41 +  val merge = merge_data;
   23.42  );
   23.43  
   23.44 -val inherit = Data.put o Data.get;
   23.45 +fun inherit contexts = Data.put (Library.foldl1 merge_data (map Data.get contexts));
   23.46 +
   23.47 +end;
   23.48  
   23.49  val get_env = Name_Space.get o #1 o Data.get;
   23.50  val get_tables = #1 oo get_env;
    24.1 --- a/src/Pure/PIDE/command.ML	Mon Sep 03 13:28:52 2018 +0100
    24.2 +++ b/src/Pure/PIDE/command.ML	Mon Sep 03 13:32:29 2018 +0100
    24.3 @@ -70,7 +70,8 @@
    24.4      val text = File.read full_path;
    24.5      val lines = split_lines text;
    24.6      val digest = SHA1.digest text;
    24.7 -  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
    24.8 +    val file_pos = Position.copy_id pos (Path.position full_path);
    24.9 +  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
   24.10    handle ERROR msg => error (msg ^ Position.here pos);
   24.11  
   24.12  val read_file = read_file_node "";
   24.13 @@ -179,7 +180,7 @@
   24.14  fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
   24.15  
   24.16  fun eval_result (Eval {eval_process, ...}) =
   24.17 -  task_context (Future.worker_subgroup ()) Lazy.force eval_process;
   24.18 +  Exn.release (Lazy.finished_result eval_process);
   24.19  
   24.20  val eval_result_command = #command o eval_result;
   24.21  val eval_result_state = #state o eval_result;
   24.22 @@ -192,6 +193,10 @@
   24.23      val res =
   24.24        if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
   24.25        else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
   24.26 +      else if Keyword.is_theory_end keywords name then
   24.27 +        (case Toplevel.reset_notepad st0 of
   24.28 +          NONE => Toplevel.reset_theory st0
   24.29 +        | some => some)
   24.30        else NONE;
   24.31    in
   24.32      (case res of
   24.33 @@ -259,10 +264,14 @@
   24.34          let
   24.35            val _ = status tr Markup.failed;
   24.36            val _ = status tr Markup.finished;
   24.37 -          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
   24.38 +          val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else ();
   24.39          in {failed = true, command = tr, state = st} end
   24.40      | SOME st' =>
   24.41          let
   24.42 +          val _ =
   24.43 +            if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso
   24.44 +              can (Toplevel.end_theory Position.none) st'
   24.45 +            then status tr Markup.finalized else ();
   24.46            val _ = status tr Markup.finished;
   24.47          in {failed = false, command = tr, state = st'} end)
   24.48    end;
   24.49 @@ -282,7 +291,8 @@
   24.50                read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
   24.51        in eval_state keywords span tr eval_state0 end;
   24.52    in
   24.53 -    Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process}
   24.54 +    Eval {command_id = command_id, exec_id = exec_id,
   24.55 +      eval_process = Lazy.lazy_name "Command.eval" process}
   24.56    end;
   24.57  
   24.58  end;
   24.59 @@ -442,7 +452,7 @@
   24.60  fun run_process execution_id exec_id process =
   24.61    let val group = Future.worker_subgroup () in
   24.62      if Execution.running execution_id exec_id [group] then
   24.63 -      ignore (task_context group Lazy.force_result process)
   24.64 +      ignore (task_context group Lazy.force_result {strict = true} process)
   24.65      else ()
   24.66    end;
   24.67  
    25.1 --- a/src/Pure/PIDE/document.ML	Mon Sep 03 13:28:52 2018 +0100
    25.2 +++ b/src/Pure/PIDE/document.ML	Mon Sep 03 13:32:29 2018 +0100
    25.3 @@ -514,28 +514,28 @@
    25.4            (fn deps => fn (name, node) =>
    25.5              if Symtab.defined required name orelse visible_node node orelse pending_result node then
    25.6                let
    25.7 -                fun body () =
    25.8 -                 (Execution.worker_task_active true name;
    25.9 -                  if forall finished_import deps then
   25.10 -                    iterate_entries (fn (_, opt_exec) => fn () =>
   25.11 -                      (case opt_exec of
   25.12 -                        SOME exec =>
   25.13 -                          if Execution.is_running execution_id
   25.14 -                          then SOME (Command.exec execution_id exec)
   25.15 -                          else NONE
   25.16 -                      | NONE => NONE)) node ()
   25.17 -                  else ();
   25.18 -                  Execution.worker_task_active false name)
   25.19 -                  handle exn =>
   25.20 -                   (Output.system_message (Runtime.exn_message exn);
   25.21 -                    Execution.worker_task_active false name;
   25.22 -                    Exn.reraise exn);
   25.23                  val future =
   25.24                    (singleton o Future.forks)
   25.25                     {name = "theory:" ^ name,
   25.26                      group = SOME (Future.new_group NONE),
   25.27                      deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
   25.28 -                    pri = 0, interrupts = false} body;
   25.29 +                    pri = 0, interrupts = false}
   25.30 +                  (fn () =>
   25.31 +                   (Execution.worker_task_active true name;
   25.32 +                    if forall finished_import deps then
   25.33 +                      iterate_entries (fn (_, opt_exec) => fn () =>
   25.34 +                        (case opt_exec of
   25.35 +                          SOME exec =>
   25.36 +                            if Execution.is_running execution_id
   25.37 +                            then SOME (Command.exec execution_id exec)
   25.38 +                            else NONE
   25.39 +                        | NONE => NONE)) node ()
   25.40 +                    else ();
   25.41 +                    Execution.worker_task_active false name)
   25.42 +                      handle exn =>
   25.43 +                       (Output.system_message (Runtime.exn_message exn);
   25.44 +                        Execution.worker_task_active false name;
   25.45 +                        Exn.reraise exn));
   25.46                in (node, SOME (Future.task_of future)) end
   25.47              else (node, NONE));
   25.48        val execution' =
   25.49 @@ -574,9 +574,12 @@
   25.50      val header = read_header node span;
   25.51      val imports = #imports header;
   25.52  
   25.53 -    fun maybe_end_theory pos st =
   25.54 -      SOME (Toplevel.end_theory pos st)
   25.55 -        handle ERROR msg => (Output.error_message msg; NONE);
   25.56 +    fun maybe_eval_result eval = Command.eval_result_state eval
   25.57 +      handle Fail _ => Toplevel.toplevel;
   25.58 +
   25.59 +    fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
   25.60 +      handle ERROR msg => (Output.error_message msg; NONE);
   25.61 +
   25.62      val parents_reports =
   25.63        imports |> map_filter (fn (import, pos) =>
   25.64          (case Thy_Info.lookup_theory import of
   25.65 @@ -584,7 +587,7 @@
   25.66              maybe_end_theory pos
   25.67                (case get_result (snd (the (AList.lookup (op =) deps import))) of
   25.68                  NONE => Toplevel.toplevel
   25.69 -              | SOME (_, eval) => Command.eval_result_state eval)
   25.70 +              | SOME (_, eval) => maybe_eval_result eval)
   25.71          | some => some)
   25.72          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
   25.73  
    26.1 --- a/src/Pure/PIDE/document.scala	Mon Sep 03 13:28:52 2018 +0100
    26.2 +++ b/src/Pure/PIDE/document.scala	Mon Sep 03 13:32:29 2018 +0100
    26.3 @@ -706,14 +706,16 @@
    26.4      def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
    26.5      def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
    26.6  
    26.7 +    def lookup_id(id: Document_ID.Generic): Option[Command.State] =
    26.8 +      commands.get(id) orElse execs.get(id)
    26.9 +
   26.10      private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
   26.11        id == st.command.id ||
   26.12        (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
   26.13  
   26.14      private def other_id(id: Document_ID.Generic)
   26.15        : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] =
   26.16 -      (execs.get(id) orElse commands.get(id)).map(st =>
   26.17 -        ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
   26.18 +      lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
   26.19  
   26.20      private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
   26.21        (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
   26.22 @@ -1077,7 +1079,7 @@
   26.23          /* find command */
   26.24  
   26.25          def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
   26.26 -          state.commands.get(id) orElse state.execs.get(id) match {
   26.27 +          state.lookup_id(id) match {
   26.28              case None => None
   26.29              case Some(st) =>
   26.30                val command = st.command
    27.1 --- a/src/Pure/PIDE/document_status.scala	Mon Sep 03 13:28:52 2018 +0100
    27.2 +++ b/src/Pure/PIDE/document_status.scala	Mon Sep 03 13:32:29 2018 +0100
    27.3 @@ -15,7 +15,7 @@
    27.4    {
    27.5      val proper_elements: Markup.Elements =
    27.6        Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    27.7 -        Markup.FINISHED, Markup.FAILED)
    27.8 +        Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
    27.9  
   27.10      val liberal_elements: Markup.Elements =
   27.11        proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
   27.12 @@ -26,6 +26,8 @@
   27.13        var accepted = false
   27.14        var warned = false
   27.15        var failed = false
   27.16 +      var canceled = false
   27.17 +      var finalized = false
   27.18        var forks = 0
   27.19        var runs = 0
   27.20        for (markup <- markup_iterator) {
   27.21 @@ -37,10 +39,20 @@
   27.22            case Markup.FINISHED => runs -= 1
   27.23            case Markup.WARNING | Markup.LEGACY => warned = true
   27.24            case Markup.FAILED | Markup.ERROR => failed = true
   27.25 +          case Markup.CANCELED => canceled = true
   27.26 +          case Markup.FINALIZED => finalized = true
   27.27            case _ =>
   27.28          }
   27.29        }
   27.30 -      Command_Status(touched, accepted, warned, failed, forks, runs)
   27.31 +      Command_Status(
   27.32 +        touched = touched,
   27.33 +        accepted = accepted,
   27.34 +        warned = warned,
   27.35 +        failed = failed,
   27.36 +        canceled = canceled,
   27.37 +        finalized = finalized,
   27.38 +        forks = forks,
   27.39 +        runs = runs)
   27.40      }
   27.41  
   27.42      val empty = make(Iterator.empty)
   27.43 @@ -58,23 +70,30 @@
   27.44      private val accepted: Boolean,
   27.45      private val warned: Boolean,
   27.46      private val failed: Boolean,
   27.47 +    private val canceled: Boolean,
   27.48 +    private val finalized: Boolean,
   27.49      forks: Int,
   27.50      runs: Int)
   27.51    {
   27.52      def + (that: Command_Status): Command_Status =
   27.53        Command_Status(
   27.54 -        touched || that.touched,
   27.55 -        accepted || that.accepted,
   27.56 -        warned || that.warned,
   27.57 -        failed || that.failed,
   27.58 -        forks + that.forks,
   27.59 -        runs + that.runs)
   27.60 +        touched = touched || that.touched,
   27.61 +        accepted = accepted || that.accepted,
   27.62 +        warned = warned || that.warned,
   27.63 +        failed = failed || that.failed,
   27.64 +        canceled = canceled || that.canceled,
   27.65 +        finalized = finalized || that.finalized,
   27.66 +        forks = forks + that.forks,
   27.67 +        runs = runs + that.runs)
   27.68  
   27.69      def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
   27.70      def is_running: Boolean = runs != 0
   27.71      def is_warned: Boolean = warned
   27.72      def is_failed: Boolean = failed
   27.73      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
   27.74 +    def is_canceled: Boolean = canceled
   27.75 +    def is_finalized: Boolean = finalized
   27.76 +    def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
   27.77    }
   27.78  
   27.79  
   27.80 @@ -94,6 +113,9 @@
   27.81        var warned = 0
   27.82        var failed = 0
   27.83        var finished = 0
   27.84 +      var canceled = false
   27.85 +      var terminated = false
   27.86 +      var finalized = false
   27.87        for (command <- node.commands.iterator) {
   27.88          val states = state.command_states(version, command)
   27.89          val status = Command_Status.merge(states.iterator.map(_.document_status))
   27.90 @@ -103,17 +125,39 @@
   27.91          else if (status.is_warned) warned += 1
   27.92          else if (status.is_finished) finished += 1
   27.93          else unprocessed += 1
   27.94 +
   27.95 +        if (status.is_canceled) canceled = true
   27.96 +        if (status.is_terminated) terminated = true
   27.97 +        if (status.is_finalized) finalized = true
   27.98        }
   27.99        val initialized = state.node_initialized(version, name)
  27.100        val consolidated = state.node_consolidated(version, name)
  27.101  
  27.102 -      Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
  27.103 +      Node_Status(
  27.104 +        unprocessed = unprocessed,
  27.105 +        running = running,
  27.106 +        warned = warned,
  27.107 +        failed = failed,
  27.108 +        finished = finished,
  27.109 +        canceled = canceled,
  27.110 +        terminated = terminated,
  27.111 +        initialized = initialized,
  27.112 +        finalized = finalized,
  27.113 +        consolidated = consolidated)
  27.114      }
  27.115    }
  27.116  
  27.117    sealed case class Node_Status(
  27.118 -    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
  27.119 -    initialized: Boolean, consolidated: Boolean)
  27.120 +    unprocessed: Int,
  27.121 +    running: Int,
  27.122 +    warned: Int,
  27.123 +    failed: Int,
  27.124 +    finished: Int,
  27.125 +    canceled: Boolean,
  27.126 +    terminated: Boolean,
  27.127 +    initialized: Boolean,
  27.128 +    finalized: Boolean,
  27.129 +    consolidated: Boolean)
  27.130    {
  27.131      def ok: Boolean = failed == 0
  27.132      def total: Int = unprocessed + running + warned + failed + finished
  27.133 @@ -121,7 +165,7 @@
  27.134      def json: JSON.Object.T =
  27.135        JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
  27.136          "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
  27.137 -        "initialized" -> initialized, "consolidated" -> consolidated)
  27.138 +        "canceled" -> canceled, "consolidated" -> consolidated)
  27.139    }
  27.140  
  27.141  
  27.142 @@ -179,6 +223,12 @@
  27.143      def apply(name: Document.Node.Name): Node_Status = rep(name)
  27.144      def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
  27.145  
  27.146 +    def quasi_consolidated(name: Document.Node.Name): Boolean =
  27.147 +      rep.get(name) match {
  27.148 +        case Some(st) => !st.finalized && st.terminated
  27.149 +        case None => false
  27.150 +      }
  27.151 +
  27.152      def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
  27.153        rep.get(name) match {
  27.154          case Some(st) if st.consolidated =>
  27.155 @@ -223,14 +273,17 @@
  27.156        var ok = 0
  27.157        var failed = 0
  27.158        var pending = 0
  27.159 +      var canceled = 0
  27.160        for (name <- rep.keysIterator) {
  27.161          overall_node_status(name) match {
  27.162            case Overall_Node_Status.ok => ok += 1
  27.163            case Overall_Node_Status.failed => failed += 1
  27.164            case Overall_Node_Status.pending => pending += 1
  27.165          }
  27.166 +        if (apply(name).canceled) canceled += 1
  27.167        }
  27.168 -      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending + ")"
  27.169 +      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
  27.170 +        ", canceled = " + canceled + ")"
  27.171      }
  27.172    }
  27.173  }
    28.1 --- a/src/Pure/PIDE/execution.ML	Mon Sep 03 13:28:52 2018 +0100
    28.2 +++ b/src/Pure/PIDE/execution.ML	Mon Sep 03 13:32:29 2018 +0100
    28.3 @@ -168,18 +168,19 @@
    28.4                  Exn.capture (Future.interruptible_task e) ()
    28.5                  |> Future.identify_result pos
    28.6                  |> Exn.map_exn Runtime.thread_context;
    28.7 +              val errors =
    28.8 +                Exn.capture (fn () =>
    28.9 +                  (case result of
   28.10 +                    Exn.Exn exn =>
   28.11 +                     (status task [Markup.failed];
   28.12 +                      status task [Markup.finished];
   28.13 +                      Output.report [Markup.markup_only (Markup.bad ())];
   28.14 +                      if exec_id = 0 then ()
   28.15 +                      else List.app (Future.error_message pos) (Runtime.exn_messages exn))
   28.16 +                  | Exn.Res _ =>
   28.17 +                      status task [Markup.finished])) ();
   28.18                val _ = status task [Markup.joined];
   28.19 -              val _ =
   28.20 -                (case result of
   28.21 -                  Exn.Exn exn =>
   28.22 -                   (status task [Markup.failed];
   28.23 -                    status task [Markup.finished];
   28.24 -                    Output.report [Markup.markup_only (Markup.bad ())];
   28.25 -                    if exec_id = 0 then ()
   28.26 -                    else List.app (Future.error_message pos) (Runtime.exn_messages exn))
   28.27 -                | Exn.Res _ =>
   28.28 -                    status task [Markup.finished])
   28.29 -            in Exn.release result end);
   28.30 +            in Exn.release errors; Exn.release result end);
   28.31  
   28.32        val _ = status (Future.task_of future) [Markup.forked];
   28.33      in future end)) ();
    29.1 --- a/src/Pure/PIDE/markup.ML	Mon Sep 03 13:28:52 2018 +0100
    29.2 +++ b/src/Pure/PIDE/markup.ML	Mon Sep 03 13:32:29 2018 +0100
    29.3 @@ -165,7 +165,9 @@
    29.4    val runningN: string val running: T
    29.5    val finishedN: string val finished: T
    29.6    val failedN: string val failed: T
    29.7 +  val canceledN: string val canceled: T
    29.8    val initializedN: string val initialized: T
    29.9 +  val finalizedN: string val finalized: T
   29.10    val consolidatedN: string val consolidated: T
   29.11    val exec_idN: string
   29.12    val initN: string
   29.13 @@ -577,8 +579,9 @@
   29.14  val (runningN, running) = markup_elem "running";
   29.15  val (finishedN, finished) = markup_elem "finished";
   29.16  val (failedN, failed) = markup_elem "failed";
   29.17 -
   29.18 +val (canceledN, canceled) = markup_elem "canceled";
   29.19  val (initializedN, initialized) = markup_elem "initialized";
   29.20 +val (finalizedN, finalized) = markup_elem "finalized";
   29.21  val (consolidatedN, consolidated) = markup_elem "consolidated";
   29.22  
   29.23  
    30.1 --- a/src/Pure/PIDE/markup.scala	Mon Sep 03 13:28:52 2018 +0100
    30.2 +++ b/src/Pure/PIDE/markup.scala	Mon Sep 03 13:32:29 2018 +0100
    30.3 @@ -424,8 +424,9 @@
    30.4    val RUNNING = "running"
    30.5    val FINISHED = "finished"
    30.6    val FAILED = "failed"
    30.7 -
    30.8 +  val CANCELED = "canceled"
    30.9    val INITIALIZED = "initialized"
   30.10 +  val FINALIZED = "finalized"
   30.11    val CONSOLIDATED = "consolidated"
   30.12  
   30.13  
    31.1 --- a/src/Pure/PIDE/rendering.scala	Mon Sep 03 13:28:52 2018 +0100
    31.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Sep 03 13:32:29 2018 +0100
    31.3 @@ -19,7 +19,7 @@
    31.4    object Color extends Enumeration
    31.5    {
    31.6      // background
    31.7 -    val unprocessed1, running1, bad, intensify, entity, active, active_result,
    31.8 +    val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
    31.9        markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
   31.10      val background_colors = values
   31.11  
   31.12 @@ -432,6 +432,7 @@
   31.13              val status = Document_Status.Command_Status.make(markups.iterator)
   31.14              if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
   31.15              else if (status.is_running) Some(Rendering.Color.running1)
   31.16 +            else if (status.is_canceled) Some(Rendering.Color.canceled)
   31.17              else opt_color
   31.18            case (_, opt_color) => opt_color
   31.19          })
    32.1 --- a/src/Pure/Pure.thy	Mon Sep 03 13:28:52 2018 +0100
    32.2 +++ b/src/Pure/Pure.thy	Mon Sep 03 13:32:29 2018 +0100
    32.3 @@ -916,7 +916,7 @@
    32.4  
    32.5  val _ =
    32.6    Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
    32.7 -    (Scan.succeed (Toplevel.forget_proof true));
    32.8 +    (Scan.succeed Toplevel.forget_proof);
    32.9  
   32.10  in end\<close>
   32.11  
    33.1 --- a/src/Pure/System/progress.scala	Mon Sep 03 13:28:52 2018 +0100
    33.2 +++ b/src/Pure/System/progress.scala	Mon Sep 03 13:32:29 2018 +0100
    33.3 @@ -21,7 +21,7 @@
    33.4    def echo(msg: String) {}
    33.5    def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
    33.6    def theory(session: String, theory: String) {}
    33.7 -  def nodes_status(nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)]) {}
    33.8 +  def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {}
    33.9  
   33.10    def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
   33.11    def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
    34.1 --- a/src/Pure/Thy/export_theory.ML	Mon Sep 03 13:28:52 2018 +0100
    34.2 +++ b/src/Pure/Thy/export_theory.ML	Mon Sep 03 13:32:29 2018 +0100
    34.3 @@ -87,7 +87,6 @@
    34.4                      XML.Elem (entity_markup space name, body))))
    34.5            |> sort (int_ord o apply2 #1) |> map #2
    34.6          end;
    34.7 -
    34.8        in if null elems then () else export_body thy export_name elems end;
    34.9  
   34.10  
   34.11 @@ -196,6 +195,25 @@
   34.12      val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
   34.13      val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
   34.14  
   34.15 +
   34.16 +    (* locales *)
   34.17 +
   34.18 +    fun encode_locale ({type_params, params, asm, defs}: Locale.content) =
   34.19 +      let
   34.20 +        val args = map #1 params;
   34.21 +        val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ the_list asm) []);
   34.22 +        val encode =
   34.23 +          let open XML.Encode Term_XML.Encode in
   34.24 +            pair (list (pair string sort))
   34.25 +              (pair (list (pair string typ))
   34.26 +                (pair (option term) (list term)))
   34.27 +          end;
   34.28 +      in encode (typargs, (args, (asm, defs))) end;
   34.29 +
   34.30 +    val _ =
   34.31 +      export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
   34.32 +        (Locale.dest_locales thy);
   34.33 +
   34.34    in () end);
   34.35  
   34.36  end;
    35.1 --- a/src/Pure/Thy/export_theory.scala	Mon Sep 03 13:28:52 2018 +0100
    35.2 +++ b/src/Pure/Thy/export_theory.scala	Mon Sep 03 13:32:29 2018 +0100
    35.3 @@ -30,9 +30,10 @@
    35.4      axioms: Boolean = true,
    35.5      facts: Boolean = true,
    35.6      classes: Boolean = true,
    35.7 -    typedefs: Boolean = true,
    35.8 +    locales: Boolean = true,
    35.9      classrel: Boolean = true,
   35.10      arities: Boolean = true,
   35.11 +    typedefs: Boolean = true,
   35.12      cache: Term.Cache = Term.make_cache()): Session =
   35.13    {
   35.14      val thys =
   35.15 @@ -42,7 +43,8 @@
   35.16            Export.read_theory_names(db, session_name).map((theory_name: String) =>
   35.17              read_theory(Export.Provider.database(db, session_name, theory_name),
   35.18                session_name, theory_name, types = types, consts = consts,
   35.19 -              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
   35.20 +              axioms = axioms, facts = facts, classes = classes, locales = locales,
   35.21 +              classrel = classrel, arities = arities, typedefs = typedefs,
   35.22                cache = Some(cache)))
   35.23          }
   35.24        })
   35.25 @@ -69,9 +71,10 @@
   35.26      axioms: List[Fact_Single],
   35.27      facts: List[Fact_Multi],
   35.28      classes: List[Class],
   35.29 -    typedefs: List[Typedef],
   35.30 +    locales: List[Locale],
   35.31      classrel: List[Classrel],
   35.32 -    arities: List[Arity])
   35.33 +    arities: List[Arity],
   35.34 +    typedefs: List[Typedef])
   35.35    {
   35.36      override def toString: String = name
   35.37  
   35.38 @@ -81,7 +84,8 @@
   35.39          consts.iterator.map(_.entity.serial) ++
   35.40          axioms.iterator.map(_.entity.serial) ++
   35.41          facts.iterator.map(_.entity.serial) ++
   35.42 -        classes.iterator.map(_.entity.serial)
   35.43 +        classes.iterator.map(_.entity.serial) ++
   35.44 +        locales.iterator.map(_.entity.serial)
   35.45  
   35.46      def cache(cache: Term.Cache): Theory =
   35.47        Theory(cache.string(name),
   35.48 @@ -91,13 +95,14 @@
   35.49          axioms.map(_.cache(cache)),
   35.50          facts.map(_.cache(cache)),
   35.51          classes.map(_.cache(cache)),
   35.52 -        typedefs.map(_.cache(cache)),
   35.53 +        locales.map(_.cache(cache)),
   35.54          classrel.map(_.cache(cache)),
   35.55 -        arities.map(_.cache(cache)))
   35.56 +        arities.map(_.cache(cache)),
   35.57 +        typedefs.map(_.cache(cache)))
   35.58    }
   35.59  
   35.60    def empty_theory(name: String): Theory =
   35.61 -    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
   35.62 +    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
   35.63  
   35.64    def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
   35.65      types: Boolean = true,
   35.66 @@ -105,9 +110,10 @@
   35.67      axioms: Boolean = true,
   35.68      facts: Boolean = true,
   35.69      classes: Boolean = true,
   35.70 -    typedefs: Boolean = true,
   35.71 +    locales: Boolean = true,
   35.72      classrel: Boolean = true,
   35.73      arities: Boolean = true,
   35.74 +    typedefs: Boolean = true,
   35.75      cache: Option[Term.Cache] = None): Theory =
   35.76    {
   35.77      val parents =
   35.78 @@ -124,9 +130,10 @@
   35.79          if (axioms) read_axioms(provider) else Nil,
   35.80          if (facts) read_facts(provider) else Nil,
   35.81          if (classes) read_classes(provider) else Nil,
   35.82 -        if (typedefs) read_typedefs(provider) else Nil,
   35.83 +        if (locales) read_locales(provider) else Nil,
   35.84          if (classrel) read_classrel(provider) else Nil,
   35.85 -        if (arities) read_arities(provider) else Nil)
   35.86 +        if (arities) read_arities(provider) else Nil,
   35.87 +        if (typedefs) read_typedefs(provider) else Nil)
   35.88      if (cache.isDefined) theory.cache(cache.get) else theory
   35.89    }
   35.90  
   35.91 @@ -154,6 +161,7 @@
   35.92      val AXIOM = Value("axiom")
   35.93      val FACT = Value("fact")
   35.94      val CLASS = Value("class")
   35.95 +    val LOCALE = Value("locale")
   35.96    }
   35.97  
   35.98    sealed case class Entity(
   35.99 @@ -316,6 +324,36 @@
  35.100        })
  35.101  
  35.102  
  35.103 +  /* locales */
  35.104 +
  35.105 +  sealed case class Locale(
  35.106 +    entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)],
  35.107 +      asm: Option[Term.Term], defs: List[Term.Term])
  35.108 +  {
  35.109 +    def cache(cache: Term.Cache): Locale =
  35.110 +      Locale(entity.cache(cache),
  35.111 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
  35.112 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
  35.113 +        asm.map(cache.term(_)),
  35.114 +        defs.map(cache.term(_)))
  35.115 +  }
  35.116 +
  35.117 +  def read_locales(provider: Export.Provider): List[Locale] =
  35.118 +    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
  35.119 +      {
  35.120 +        val (entity, body) = decode_entity(Kind.LOCALE, tree)
  35.121 +        val (typargs, (args, (asm, defs))) =
  35.122 +        {
  35.123 +          import XML.Decode._
  35.124 +          import Term_XML.Decode._
  35.125 +          pair(list(pair(string, sort)),
  35.126 +            pair(list(pair(string, typ)),
  35.127 +              pair(option(term), list(term))))(body)
  35.128 +        }
  35.129 +        Locale(entity, typargs, args, asm, defs)
  35.130 +      })
  35.131 +
  35.132 +
  35.133    /* sort algebra */
  35.134  
  35.135    sealed case class Classrel(class_name: String, super_names: List[String])
    36.1 --- a/src/Pure/Thy/thy_resources.scala	Mon Sep 03 13:28:52 2018 +0100
    36.2 +++ b/src/Pure/Thy/thy_resources.scala	Mon Sep 03 13:32:29 2018 +0100
    36.3 @@ -111,6 +111,8 @@
    36.4            master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
    36.5        val dep_theories_set = dep_theories.toSet
    36.6  
    36.7 +      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
    36.8 +
    36.9        val result = Future.promise[Theories_Result]
   36.10  
   36.11        def check_state(beyond_limit: Boolean = false)
   36.12 @@ -118,7 +120,11 @@
   36.13          val state = session.current_state()
   36.14          state.stable_tip_version match {
   36.15            case Some(version) =>
   36.16 -            if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
   36.17 +            if (beyond_limit ||
   36.18 +                dep_theories.forall(name =>
   36.19 +                  state.node_consolidated(version, name) ||
   36.20 +                  nodes_status_update.value._1.quasi_consolidated(name)))
   36.21 +            {
   36.22                val nodes =
   36.23                  for (name <- dep_theories)
   36.24                  yield (name -> Document_Status.Node_Status.make(state, version, name))
   36.25 @@ -144,12 +150,10 @@
   36.26  
   36.27        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
   36.28  
   36.29 -      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
   36.30 -
   36.31        val delay_nodes_status =
   36.32          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
   36.33            val (nodes_status, names) = nodes_status_update.value
   36.34 -          progress.nodes_status(names.map(name => (name -> nodes_status(name))))
   36.35 +          progress.nodes_status(nodes_status, names)
   36.36          }
   36.37  
   36.38        val consumer =
   36.39 @@ -160,19 +164,19 @@
   36.40                val state = snapshot.state
   36.41                val version = snapshot.version
   36.42  
   36.43 -              if (nodes_status_delay >= Time.zero) {
   36.44 -                nodes_status_update.change(
   36.45 -                  { case upd @ (nodes_status, _) =>
   36.46 -                      val domain =
   36.47 -                        if (nodes_status.is_empty) dep_theories_set
   36.48 -                        else changed.nodes.iterator.filter(dep_theories_set).toSet
   36.49 -                      val upd1 =
   36.50 -                        nodes_status.update(resources.session_base, state, version,
   36.51 -                          domain = Some(domain), trim = changed.assignment).getOrElse(upd)
   36.52 -                      if (upd == upd1) upd
   36.53 -                      else { delay_nodes_status.invoke; upd1 }
   36.54 -                  })
   36.55 -              }
   36.56 +              nodes_status_update.change(
   36.57 +                { case upd @ (nodes_status, _) =>
   36.58 +                    val domain =
   36.59 +                      if (nodes_status.is_empty) dep_theories_set
   36.60 +                      else changed.nodes.iterator.filter(dep_theories_set).toSet
   36.61 +                    val upd1 =
   36.62 +                      nodes_status.update(resources.session_base, state, version,
   36.63 +                        domain = Some(domain), trim = changed.assignment).getOrElse(upd)
   36.64 +                    if (nodes_status_delay >= Time.zero && upd != upd1)
   36.65 +                      delay_nodes_status.invoke
   36.66 +
   36.67 +                    upd1
   36.68 +                })
   36.69  
   36.70                val check_theories =
   36.71                  (for {
    37.1 --- a/src/Pure/Tools/dump.scala	Mon Sep 03 13:28:52 2018 +0100
    37.2 +++ b/src/Pure/Tools/dump.scala	Mon Sep 03 13:32:29 2018 +0100
    37.3 @@ -136,7 +136,7 @@
    37.4      else {
    37.5        for {
    37.6          (name, status) <- theories_result.nodes if !status.ok
    37.7 -        (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
    37.8 +        (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
    37.9        } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
   37.10  
   37.11        session_result.copy(rc = session_result.rc max 1)
    38.1 --- a/src/Pure/Tools/server.scala	Mon Sep 03 13:28:52 2018 +0100
    38.2 +++ b/src/Pure/Tools/server.scala	Mon Sep 03 13:32:29 2018 +0100
    38.3 @@ -274,11 +274,9 @@
    38.4          (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
    38.5  
    38.6      override def nodes_status(
    38.7 -      nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)])
    38.8 +      nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name])
    38.9      {
   38.10 -      val json =
   38.11 -        for ((name, status) <- nodes_status)
   38.12 -        yield name.json + ("status" -> status.json)
   38.13 +      val json = names.map(name => name.json + ("status" -> nodes_status(name).json))
   38.14        context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
   38.15      }
   38.16  
    39.1 --- a/src/Tools/VSCode/extension/README.md	Mon Sep 03 13:28:52 2018 +0100
    39.2 +++ b/src/Tools/VSCode/extension/README.md	Mon Sep 03 13:32:29 2018 +0100
    39.3 @@ -1,15 +1,14 @@
    39.4  # Isabelle Prover IDE support
    39.5  
    39.6  This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
    39.7 -requires Isabelle2018.
    39.8 +requires a repository version of Isabelle.
    39.9  
   39.10  The implementation is centered around the VSCode Language Server protocol, but
   39.11  with many add-ons that are specific to VSCode and Isabelle/PIDE.
   39.12  
   39.13  See also:
   39.14  
   39.15 -  * <https://isabelle.in.tum.de/website-Isabelle2018>
   39.16 -  * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Tools/VSCode>
   39.17 +  * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
   39.18    * <https://github.com/Microsoft/language-server-protocol>
   39.19  
   39.20  
   39.21 @@ -59,8 +58,7 @@
   39.22  
   39.23  ### Isabelle/VSCode Installation
   39.24  
   39.25 -  * Download Isabelle2018 from <https://isabelle.in.tum.de/website-Isabelle2018>
   39.26 -    or any of its mirror sites.
   39.27 +  * Download a recent Isabelle development snapshot from <http://isabelle.in.tum.de/devel/release_snapshot>
   39.28  
   39.29    * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
   39.30    the logic image is built properly and Isabelle works as expected.
   39.31 @@ -69,7 +67,7 @@
   39.32  
   39.33    * Open the VSCode *Extensions* view and install the following:
   39.34  
   39.35 -      + *Isabelle2018* (needs to fit to the underlying Isabelle release).
   39.36 +      + *Isabelle*.
   39.37  
   39.38        + *Prettify Symbols Mode* (important for display of Isabelle symbols).
   39.39  
   39.40 @@ -90,17 +88,17 @@
   39.41  
   39.42        + Linux:
   39.43          ```
   39.44 -        "isabelle.home": "/home/makarius/Isabelle2018"
   39.45 +        "isabelle.home": "/home/makarius/Isabelle"
   39.46          ```
   39.47  
   39.48        + Mac OS X:
   39.49          ```
   39.50 -        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018"
   39.51 +        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
   39.52          ```
   39.53  
   39.54        + Windows:
   39.55          ```
   39.56 -        "isabelle.home": "C:\\Users\\makarius\\Isabelle2018"
   39.57 +        "isabelle.home": "C:\\Users\\makarius\\Isabelle"
   39.58          ```
   39.59  
   39.60    * Restart the VSCode application to ensure that all extensions are properly
    40.1 --- a/src/Tools/VSCode/extension/package.json	Mon Sep 03 13:28:52 2018 +0100
    40.2 +++ b/src/Tools/VSCode/extension/package.json	Mon Sep 03 13:32:29 2018 +0100
    40.3 @@ -1,6 +1,6 @@
    40.4  {
    40.5 -    "name": "Isabelle2018",
    40.6 -    "displayName": "Isabelle2018",
    40.7 +    "name": "isabelle",
    40.8 +    "displayName": "Isabelle",
    40.9      "description": "Isabelle Prover IDE",
   40.10      "keywords": [
   40.11          "theorem prover",
   40.12 @@ -10,7 +10,7 @@
   40.13          "document preparation"
   40.14      ],
   40.15      "icon": "isabelle.png",
   40.16 -    "version": "1.1.0",
   40.17 +    "version": "1.1.1",
   40.18      "publisher": "makarius",
   40.19      "license": "MIT",
   40.20      "repository": {
   40.21 @@ -250,6 +250,14 @@
   40.22                      "type": "string",
   40.23                      "default": "rgba(255, 160, 160, 0.40)"
   40.24                  },
   40.25 +                "isabelle.canceled_light_color": {
   40.26 +                    "type": "string",
   40.27 +                    "default": "rgba(255, 106, 106, 0.40)"
   40.28 +                },
   40.29 +                "isabelle.canceled_dark_color": {
   40.30 +                    "type": "string",
   40.31 +                    "default": "rgba(255, 106, 106, 0.40)"
   40.32 +                },
   40.33                  "isabelle.bad_light_color": {
   40.34                      "type": "string",
   40.35                      "default": "rgba(255, 106, 106, 0.40)"
    41.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Mon Sep 03 13:28:52 2018 +0100
    41.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Mon Sep 03 13:32:29 2018 +0100
    41.3 @@ -13,6 +13,7 @@
    41.4  const background_colors = [
    41.5    "unprocessed1",
    41.6    "running1",
    41.7 +  "canceled",
    41.8    "bad",
    41.9    "intensify",
   41.10    "quoted",
    42.1 --- a/src/Tools/jEdit/etc/options	Mon Sep 03 13:28:52 2018 +0100
    42.2 +++ b/src/Tools/jEdit/etc/options	Mon Sep 03 13:32:29 2018 +0100
    42.3 @@ -95,6 +95,7 @@
    42.4  option error_message_color : string = "FFC1C1FF"
    42.5  option spell_checker_color : string = "0000FFFF"
    42.6  option bad_color : string = "FF6A6A64"
    42.7 +option canceled_color : string = "FF6A6A64"
    42.8  option intensify_color : string = "FFCC6664"
    42.9  option entity_color : string = "CCD9FF80"
   42.10  option entity_ref_color : string = "800080FF"