--- 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: =^(
--- 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
--- 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
--- 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')"
--- 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)"
--- 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