# HG changeset patch
# User wenzelm
# Date 1376838010 -7200
# Node ID 98fc4753334252b6fae498dc23d199e778e0688e
# Parent  6a3410845bb26b9f88b2ead447f912858df9bfe2# Parent  e62c7a4b6697e62e7267a08ee2a4e0fcf0101e13
merged

diff -r 6a3410845bb2 -r 98fc47533342 etc/symbols
--- a/etc/symbols	Sun Aug 18 15:35:01 2013 +0200
+++ b/etc/symbols	Sun Aug 18 17:00:10 2013 +0200
@@ -350,9 +350,9 @@
 \<cedilla>              code: 0x0000b8
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
-\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText  abbrev: =_
-\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText  abbrev: =^
-\<^bold>                code: 0x002759  group: control  font: IsabelleText  abbrev: -.
+\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
+\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
+\<^bold>                code: 0x002759  group: control  font: IsabelleText
 \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
diff -r 6a3410845bb2 -r 98fc47533342 src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Sun Aug 18 15:35:01 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy	Sun Aug 18 17:00:10 2013 +0200
@@ -881,8 +881,7 @@
   The @{text "TYPE"} constructor is the canonical representative of
   the unspecified type @{text "\<alpha> itself"}; it essentially injects the
   language of types into that of terms.  There is specific notation
-  @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
- itself\<^esub>"}.
+  @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> itself\<^esub>"}.
   Although being devoid of any particular meaning, the term @{text
   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal
diff -r 6a3410845bb2 -r 98fc47533342 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Sun Aug 18 15:35:01 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Sun Aug 18 17:00:10 2013 +0200
@@ -800,7 +800,7 @@
   reasoning.}
 
   Currying gives some flexiblity due to \emph{partial application}.  A
-  function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^bsub>2\<^esub> \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
+  function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
   and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to another function
   etc.  How well this works in practice depends on the order of
   arguments.  In the worst case, arguments are arranged erratically,
@@ -904,8 +904,8 @@
   parametrized by arguments of type @{text "\<alpha>"}.  Given @{text "a: \<alpha>"}
   the partial application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates
   homogeneously on @{text "\<beta>"}.  This can be iterated naturally over a
-  list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f
-  a\<^bsub>n\<^esub>\<^bsub>\<^esub>"}.  The latter expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}.
+  list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f a\<^sub>n"}.
+  The latter expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}.
   It can be applied to an initial configuration @{text "b: \<beta>"} to
   start the iteration over the given list of arguments: each @{text
   "a"} in @{text "a\<^sub>1, \<dots>, a\<^sub>n"} is applied consecutively by updating a
diff -r 6a3410845bb2 -r 98fc47533342 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Aug 18 15:35:01 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Aug 18 17:00:10 2013 +0200
@@ -34,7 +34,7 @@
 lemma gather_start [no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
   by simp
 
-text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
+text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}*}
 lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
 lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
@@ -46,7 +46,7 @@
 lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
 lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
-text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
+text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}*}
 lemma pinf_gt[no_atp]:  "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
 lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
@@ -351,7 +351,7 @@
 
 lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"} *}
 lemma pinf_conj[no_atp]:
   assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
@@ -402,7 +402,7 @@
 lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
 
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"} *}
 lemma minf_conj[no_atp]:
   assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
     and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
diff -r 6a3410845bb2 -r 98fc47533342 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sun Aug 18 15:35:01 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sun Aug 18 17:00:10 2013 +0200
@@ -194,35 +194,35 @@
 | "\<down>\<^sub>e (Suc n) k \<Gamma> = \<down>\<^sub>e n k (\<Gamma>[k \<mapsto>\<^sub>\<tau> Top]\<^sub>e)"
 
 inductive
-  well_formed :: "env \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub> _" [50, 50] 50)
+  well_formed :: "env \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>w\<^sub>f _" [50, 50] 50)
 where
-  wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
-| wf_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
-| wf_arrow: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
-| wf_all: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> TVarB T \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
+  wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f TVar i"
+| wf_Top: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f Top"
+| wf_arrow: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f T \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f U \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f T \<rightarrow> U"
+| wf_all: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f T \<Longrightarrow> TVarB T \<Colon> \<Gamma> \<turnstile>\<^sub>w\<^sub>f U \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f (\<forall><:T. U)"
 
 inductive
-  well_formedE :: "env \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub>" [50] 50)
-  and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wfB\<^esub> _" [50, 50] 50)
+  well_formedE :: "env \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>w\<^sub>f" [50] 50)
+  and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>w\<^sub>f\<^sub>B _" [50, 50] 50)
 where
-  "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<equiv> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> type_ofB B"
-| wf_Nil: "[] \<turnstile>\<^bsub>wf\<^esub>"
-| wf_Cons: "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
+  "\<Gamma> \<turnstile>\<^sub>w\<^sub>f\<^sub>B B \<equiv> \<Gamma> \<turnstile>\<^sub>w\<^sub>f type_ofB B"
+| wf_Nil: "[] \<turnstile>\<^sub>w\<^sub>f"
+| wf_Cons: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f\<^sub>B B \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^sub>w\<^sub>f"
 
 inductive_cases well_formed_cases:
-  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
-  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
-  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
-  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
+  "\<Gamma> \<turnstile>\<^sub>w\<^sub>f TVar i"
+  "\<Gamma> \<turnstile>\<^sub>w\<^sub>f Top"
+  "\<Gamma> \<turnstile>\<^sub>w\<^sub>f T \<rightarrow> U"
+  "\<Gamma> \<turnstile>\<^sub>w\<^sub>f (\<forall><:T. U)"
 
 inductive_cases well_formedE_cases:
-  "B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
+  "B \<Colon> \<Gamma> \<turnstile>\<^sub>w\<^sub>f"
 
 inductive
   subtyping :: "env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ <: _" [50, 50, 50] 50)
 where
-  SA_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
-| SA_refl_TVar: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i"
+  SA_Top: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
+| SA_refl_TVar: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>w\<^sub>f TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i"
 | SA_trans_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB U\<rfloor> \<Longrightarrow>
     \<Gamma> \<turnstile> \<up>\<^sub>\<tau> (Suc i) 0 U <: T \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: T"
 | SA_arrow: "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2"
@@ -232,7 +232,7 @@
 inductive
   typing :: "env \<Rightarrow> trm \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
 where
-  T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^sub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
+  T_Var: "\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^sub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
 | T_Abs: "VarB T\<^sub>1 \<Colon> \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^sub>1. t\<^sub>2) : T\<^sub>1 \<rightarrow> \<down>\<^sub>\<tau> 1 0 T\<^sub>2"
 | T_App: "\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>11 \<rightarrow> T\<^sub>12 \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11 \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 \<bullet> t\<^sub>2 : T\<^sub>12"
 | T_TAbs: "TVarB T\<^sub>1 \<Colon> \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^sub>1. t\<^sub>2) : (\<forall><:T\<^sub>1. T\<^sub>2)"
diff -r 6a3410845bb2 -r 98fc47533342 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Aug 18 15:35:01 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Aug 18 17:00:10 2013 +0200
@@ -35,7 +35,10 @@
   @volatile var plugin: Plugin = null
   @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
 
-  def options_changed() { session.global_options.event(Session.Global_Options(options.value)) }
+  def options_changed() {
+    session.global_options.event(Session.Global_Options(options.value))
+    plugin.load_theories()
+  }
 
   def thy_load(): JEdit_Thy_Load =
     session.thy_load.asInstanceOf[JEdit_Thy_Load]
@@ -132,41 +135,45 @@
       PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
     }
 
+  def load_theories() { Swing_Thread.later { delay_load.invoke() }}
+
   private lazy val delay_load =
     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
-      val view = jEdit.getActiveView()
+      if (Isabelle.continuous_checking) {
+        val view = jEdit.getActiveView()
 
-      val buffers = JEdit_Lib.jedit_buffers().toList
-      if (buffers.forall(_.isLoaded)) {
-        def loaded_buffer(name: String): Boolean =
-          buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
+        val buffers = JEdit_Lib.jedit_buffers().toList
+        if (buffers.forall(_.isLoaded)) {
+          def loaded_buffer(name: String): Boolean =
+            buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
 
-        val thys =
-          for (buffer <- buffers; model <- PIDE.document_model(buffer))
-            yield model.node_name
+          val thys =
+            for (buffer <- buffers; model <- PIDE.document_model(buffer))
+              yield model.node_name
 
-        val thy_info = new Thy_Info(PIDE.thy_load)
-        // FIXME avoid I/O in Swing thread!?!
-        val files = thy_info.dependencies(thys).deps.map(_.name.node).
-          filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
+          val thy_info = new Thy_Info(PIDE.thy_load)
+          // FIXME avoid I/O in Swing thread!?!
+          val files = thy_info.dependencies(thys).deps.map(_.name.node).
+            filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
 
-        if (!files.isEmpty) {
-          val files_list = new ListView(files.sorted)
-          for (i <- 0 until files.length)
-            files_list.selection.indices += i
+          if (!files.isEmpty) {
+            val files_list = new ListView(files.sorted)
+            for (i <- 0 until files.length)
+              files_list.selection.indices += i
 
-          val answer =
-            GUI.confirm_dialog(view,
-              "Auto loading of required files",
-              JOptionPane.YES_NO_OPTION,
-              "The following files are required to resolve theory imports.",
-              "Reload selected files now?",
-              new ScrollPane(files_list))
-          if (answer == 0) {
-            files.foreach(file =>
-              if (files_list.selection.items.contains(file))
-                jEdit.openFile(null: View, file))
+            val answer =
+              GUI.confirm_dialog(view,
+                "Auto loading of required files",
+                JOptionPane.YES_NO_OPTION,
+                "The following files are required to resolve theory imports.",
+                "Reload selected files now?",
+                new ScrollPane(files_list))
+            if (answer == 0) {
+              files.foreach(file =>
+                if (files_list.selection.items.contains(file))
+                  jEdit.openFile(null: View, file))
+            }
           }
         }
       }
@@ -239,7 +246,7 @@
           if (PIDE.session.is_ready) {
             val buffer = msg.getBuffer
             if (buffer != null && !buffer.isLoading) delay_init.invoke()
-            Swing_Thread.later { delay_load.invoke() }
+            load_theories()
           }
 
         case msg: EditPaneUpdate