--- a/doc-src/Locales/Locales/Examples.thy Wed Jan 21 16:50:09 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Wed Jan 21 16:51:45 2009 +0100
@@ -608,7 +608,7 @@
and @{text lattice} be placed between @{text partial_order}
and @{text total_order}, as shown in Figure~\ref{fig:lattices}(b).
Changes to the locale hierarchy may be declared
- with the \isakeyword{interpretation} command. *}
+ with the \isakeyword{sublocale} command. *}
sublocale %visible total_order \<subseteq> lattice
--- a/doc-src/Locales/Locales/Examples3.thy Wed Jan 21 16:50:09 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Wed Jan 21 16:51:45 2009 +0100
@@ -178,8 +178,6 @@
nat_dvd_join_eq} are named since they are handy in the proof of
the subsequent interpretation. *}
-ML %invisible {* set quick_and_dirty *}
-
(*
definition
is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -200,8 +198,6 @@
lemma %invisible gcd_lcm_distr:
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
-ML %invisible {* reset quick_and_dirty *}
-
interpretation %visible nat_dvd:
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
apply unfold_locales
@@ -262,7 +258,7 @@
preserving maps can be declared in the following way. *}
locale order_preserving =
- partial_order + po': partial_order le' for le' (infixl "\<preceq>" 50) +
+ le: partial_order + le': partial_order le' for le' (infixl "\<preceq>" 50) +
fixes \<phi> :: "'a \<Rightarrow> 'b"
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
@@ -288,8 +284,7 @@
obtained by appending the conclusions of the left locale and of the
right locale. *}
-text {* % FIXME needs update
- The locale @{text order_preserving} contains theorems for both
+text {* The locale @{text order_preserving} contains theorems for both
orders @{text \<sqsubseteq>} and @{text \<preceq>}. How can one refer to a theorem for
a particular order, @{text \<sqsubseteq>} or @{text \<preceq>}? Names in locales are
qualified by the locale parameters. More precisely, a name is
@@ -298,8 +293,8 @@
context %invisible order_preserving begin
-text {* % FIXME needs update?
- @{thm [source] less_le_trans}: @{thm less_le_trans}
+text {*
+ @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
@{thm [source] hom_le}: @{thm hom_le}
*}
@@ -307,12 +302,11 @@
text {* When renaming a locale, the morphism is also applied
to the qualifiers. Hence theorems for the partial order @{text \<preceq>}
are qualified by @{text le'}. For example, @{thm [source]
- po'.less_le_trans}: @{thm [display, indent=2] po'.less_le_trans} *}
+ le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
end %invisible
-text {* % FIXME needs update?
- This example reveals that there is no infix syntax for the strict
+text {* This example reveals that there is no infix syntax for the strict
version of @{text \<preceq>}! This can, of course, not be introduced
automatically, but it can be declared manually through an abbreviation.
*}
@@ -321,7 +315,7 @@
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
text {* Now the theorem is displayed nicely as
- @{thm [locale=order_preserving] po'.less_le_trans}. *}
+ @{thm [locale=order_preserving] le'.less_le_trans}. *}
text {* Not only names of theorems are qualified. In fact, all names
are qualified, in particular names introduced by definitions and
@@ -333,7 +327,7 @@
text {* Two more locales illustrate working with locale expressions.
A map @{text \<phi>} is a lattice homomorphism if it preserves meet and join. *}
- locale lattice_hom = lattice + lat'!: lattice le' for le' (infixl "\<preceq>" 50) +
+ locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
fixes \<phi>
assumes hom_meet:
"\<phi> (lattice.meet le x y) = lattice.meet le' (\<phi> x) (\<phi> y)"
@@ -341,9 +335,9 @@
"\<phi> (lattice.join le x y) = lattice.join le' (\<phi> x) (\<phi> y)"
abbreviation (in lattice_hom)
- meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> lat'.meet"
+ meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
abbreviation (in lattice_hom)
- join' (infixl "\<squnion>''" 50) where "join' \<equiv> lat'.join"
+ join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
text {* A homomorphism is an endomorphism if both orders coincide. *}
@@ -400,17 +394,17 @@
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
fix x y
assume "x \<sqsubseteq> y"
- then have "y = (x \<squnion> y)" by (simp add: join_connection)
+ then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
- then show "\<phi> x \<preceq> \<phi> y" by (simp add: lat'.join_connection)
+ then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
qed
text {* Theorems and other declarations --- syntax, in particular ---
from the locale @{text order_preserving} are now active in @{text
lattice_hom}, for example
- @{thm [locale=lattice_hom, source] lat'.less_le_trans}:
- @{thm [locale=lattice_hom] lat'.less_le_trans}
+ @{thm [locale=lattice_hom, source] le'.less_le_trans}:
+ @{thm [locale=lattice_hom] le'.less_le_trans}
*}
@@ -450,7 +444,9 @@
\textit{attr-name} & ::=
& \textit{name} $|$ \textit{attribute} $|$
- \textit{name} \textit{attribute} \\[2ex]
+ \textit{name} \textit{attribute} \\
+ \textit{qualifier} & ::=
+ & \textit{name} [``\textbf{!}''] \\[2ex]
\multicolumn{3}{l}{Context Elements} \\
@@ -490,19 +486,23 @@
\multicolumn{3}{l}{Locale Expressions} \\
- \textit{rename} & ::=
- & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\
- \textit{expr} & ::=
- & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\
- \textit{renamed-expr} & ::=
- & ( \textit{qualified-name} $|$
- ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex]
+ \textit{pos-insts} & ::=
+ & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
+ \textit{named-insts} & ::=
+ & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
+ ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
+ \textit{instance} & ::=
+ & [ \textit{qualifier} \textbf{:} ]
+ \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+ \textit{expression} & ::=
+ & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
+ [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
\multicolumn{3}{l}{Declaration of Locales} \\
\textit{locale} & ::=
& \textit{element}$^+$ \\
- & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
+ & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
\textit{toplevel} & ::=
& \textbf{locale} \textit{name} [ ``\textbf{=}''
\textit{locale} ] \\[2ex]
@@ -511,19 +511,17 @@
\textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
\textit{prop} \\
- \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$
- ``\textbf{]}'' ] \\
- & & [ \textbf{where} \textit{equation} ( \textbf{and}
- \textit{equation} )$^*$ ] \\
+ \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and}
+ \textit{equation} )$^*$ \\
\textit{toplevel} & ::=
- & \textbf{interpretation} \textit{name} ( ``$<$'' $|$
- ``$\subseteq$'' ) \textit{expr} \textit{proof} \\
+ & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
+ ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
& |
- & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ]
- \textit{expr} \textit{insts} \textit{proof} \\
+ & \textbf{interpretation}
+ \textit{expression} [ \textit{equations} ] \textit{proof} \\
& |
- & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ]
- \textit{expr} \textit{insts} \textit{proof} \\[2ex]
+ & \textbf{interpret}
+ \textit{expression} \textit{proof} \\[2ex]
\multicolumn{3}{l}{Diagnostics} \\
@@ -533,7 +531,7 @@
\end{tabular}
\end{center}
\hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abridged).}
\label{tab:commands}
\end{table}
*}
--- a/doc-src/Locales/Locales/ROOT.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/doc-src/Locales/Locales/ROOT.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,4 +1,4 @@
no_document use_thy "GCD";
use_thy "Examples1";
use_thy "Examples2";
-use_thy "Examples3";
+setmp_noncritical quick_and_dirty true use_thy "Examples3";
--- a/doc-src/Locales/Locales/document/Examples.tex Wed Jan 21 16:50:09 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex Wed Jan 21 16:51:45 2009 +0100
@@ -1213,7 +1213,7 @@
and \isa{lattice} be placed between \isa{partial{\isacharunderscore}order}
and \isa{total{\isacharunderscore}order}, as shown in Figure~\ref{fig:lattices}(b).
Changes to the locale hierarchy may be declared
- with the \isakeyword{interpretation} command.%
+ with the \isakeyword{sublocale} command.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples3.tex Wed Jan 21 16:50:09 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Jan 21 16:51:45 2009 +0100
@@ -362,18 +362,10 @@
\endisadeliminvisible
%
\isataginvisible
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ set\ quick{\isacharunderscore}and{\isacharunderscore}dirty\ {\isacharverbatimclose}\isanewline
-\isanewline
-\isanewline
-\isanewline
\isacommand{lemma}\isamarkupfalse%
\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}gcd\ x\ {\isacharparenleft}lcm\ y\ z{\isacharparenright}\ {\isacharequal}\ lcm\ {\isacharparenleft}gcd\ x\ y{\isacharparenright}\ {\isacharparenleft}gcd\ x\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\ reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -383,7 +375,7 @@
\isanewline
%
\isadelimvisible
-\ \ \isanewline
+\isanewline
%
\endisadelimvisible
%
@@ -476,7 +468,7 @@
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
\ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
-\ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ po{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
+\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
\begin{isamarkuptext}%
@@ -505,8 +497,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-% FIXME needs update
- The locale \isa{order{\isacharunderscore}preserving} contains theorems for both
+The locale \isa{order{\isacharunderscore}preserving} contains theorems for both
orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}. How can one refer to a theorem for
a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}? Names in locales are
qualified by the locale parameters. More precisely, a name is
@@ -530,8 +521,7 @@
\endisadeliminvisible
%
\begin{isamarkuptext}%
-% FIXME needs update?
- \isa{less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z}
+\isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z}
\isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}%
\end{isamarkuptext}%
@@ -540,7 +530,7 @@
\begin{isamarkuptext}%
When renaming a locale, the morphism is also applied
to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}}
- are qualified by \isa{le{\isacharprime}}. For example, \isa{po{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
+ are qualified by \isa{le{\isacharprime}}. For example, \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
\ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
\isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
\end{isabelle}%
@@ -562,8 +552,7 @@
\endisadeliminvisible
%
\begin{isamarkuptext}%
-% FIXME needs update?
- This example reveals that there is no infix syntax for the strict
+This example reveals that there is no infix syntax for the strict
version of \isa{{\isasympreceq}}! This can, of course, not be introduced
automatically, but it can be declared manually through an abbreviation.%
\end{isamarkuptext}%
@@ -592,7 +581,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lat{\isacharprime}{\isacharbang}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
+\ lattice{\isacharunderscore}hom\ {\isacharequal}\ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
@@ -601,10 +590,10 @@
\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
-\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
+\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
-\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}join{\isachardoublequoteclose}%
+\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}%
\begin{isamarkuptext}%
A homomorphism is an endomorphism if both orders coincide.%
\end{isamarkuptext}%
@@ -678,7 +667,7 @@
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ join{\isacharunderscore}connection{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
@@ -686,7 +675,7 @@
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ lat{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -700,7 +689,7 @@
Theorems and other declarations --- syntax, in particular ---
from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
- \isa{lat{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+ \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
\isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -744,7 +733,9 @@
\textit{attr-name} & ::=
& \textit{name} $|$ \textit{attribute} $|$
- \textit{name} \textit{attribute} \\[2ex]
+ \textit{name} \textit{attribute} \\
+ \textit{qualifier} & ::=
+ & \textit{name} [``\textbf{!}''] \\[2ex]
\multicolumn{3}{l}{Context Elements} \\
@@ -784,19 +775,23 @@
\multicolumn{3}{l}{Locale Expressions} \\
- \textit{rename} & ::=
- & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\
- \textit{expr} & ::=
- & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\
- \textit{renamed-expr} & ::=
- & ( \textit{qualified-name} $|$
- ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex]
+ \textit{pos-insts} & ::=
+ & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
+ \textit{named-insts} & ::=
+ & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
+ ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
+ \textit{instance} & ::=
+ & [ \textit{qualifier} \textbf{:} ]
+ \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+ \textit{expression} & ::=
+ & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
+ [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
\multicolumn{3}{l}{Declaration of Locales} \\
\textit{locale} & ::=
& \textit{element}$^+$ \\
- & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
+ & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
\textit{toplevel} & ::=
& \textbf{locale} \textit{name} [ ``\textbf{=}''
\textit{locale} ] \\[2ex]
@@ -805,19 +800,17 @@
\textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
\textit{prop} \\
- \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$
- ``\textbf{]}'' ] \\
- & & [ \textbf{where} \textit{equation} ( \textbf{and}
- \textit{equation} )$^*$ ] \\
+ \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and}
+ \textit{equation} )$^*$ \\
\textit{toplevel} & ::=
- & \textbf{interpretation} \textit{name} ( ``$<$'' $|$
- ``$\subseteq$'' ) \textit{expr} \textit{proof} \\
+ & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
+ ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
& |
- & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ]
- \textit{expr} \textit{insts} \textit{proof} \\
+ & \textbf{interpretation}
+ \textit{expression} [ \textit{equations} ] \textit{proof} \\
& |
- & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ]
- \textit{expr} \textit{insts} \textit{proof} \\[2ex]
+ & \textbf{interpret}
+ \textit{expression} \textit{proof} \\[2ex]
\multicolumn{3}{l}{Diagnostics} \\
@@ -827,7 +820,7 @@
\end{tabular}
\end{center}
\hrule
-\caption{Syntax of Locale Commands.}
+\caption{Syntax of Locale Commands (abridged).}
\label{tab:commands}
\end{table}%
\end{isamarkuptext}%
--- a/doc-src/Locales/Locales/document/root.tex Wed Jan 21 16:50:09 2009 +0100
+++ b/doc-src/Locales/Locales/document/root.tex Wed Jan 21 16:51:45 2009 +0100
@@ -22,14 +22,17 @@
\begin{document}
-\title{Tutorial to Locales and Locale Interpretation}
+\title{Tutorial to Locales and Locale Interpretation \\[1ex]
+ \large 2nd revision, for Isabelle 2009}
\author{Clemens Ballarin}
\date{}
\maketitle
+%\thispagestyle{myheadings}
+%\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
\thispagestyle{myheadings}
-\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
+\markright{This tutorial is currently not consistent.}
\begin{abstract}
Locales are Isabelle's mechanism to deal with parametric theories.
@@ -40,6 +43,10 @@
This tutorial is intended for locale novices; familiarity with
Isabelle and Isar is presumed.
+ The 2nd revision accommodates changes introduced by the locales
+ reimplementation for Isabelle 2009. Most notably, in complex
+ specifications (\emph{locale expressions}) renaming has been
+ generalised to instantiation.
\end{abstract}
\parindent 0pt\parskip 0.5ex
--- a/src/Pure/Concurrent/mailbox.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Concurrent/mailbox.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Concurrent/mailbox.ML
- ID: $Id$
Author: Makarius
Message exchange via mailbox, with non-blocking send (due to unbounded
--- a/src/Pure/Concurrent/simple_thread.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Concurrent/simple_thread.ML
- ID: $Id$
Author: Makarius
Simplified thread operations.
--- a/src/Pure/Concurrent/synchronized.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Concurrent/synchronized.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Concurrent/synchronized.ML
- ID: $Id$
Author: Fabian Immler and Makarius
State variables with synchronized access.
--- a/src/Pure/General/symbol.scala Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/General/symbol.scala Wed Jan 21 16:51:45 2009 +0100
@@ -78,9 +78,9 @@
/** Symbol interpretation **/
- class Interpretation(isabelle_system: IsabelleSystem) {
-
- private var symbols = new HashMap[String, HashMap[String, String]]
+ class Interpretation(symbol_decls: Iterator[String])
+ {
+ private val symbols = new HashMap[String, HashMap[String, String]]
private var decoder: Recoder = null
private var encoder: Recoder = null
@@ -94,10 +94,11 @@
private val blank_pattern = compile(""" \s+ """)
private val key_pattern = compile(""" (.+): """)
- private def read_line(line: String) = {
- def err() = error("Bad symbol specification (line " + line + ")")
+ private def read_decl(decl: String) = {
+ def err() = error("Bad symbol declaration: " + decl)
- def read_props(props: List[String], tab: HashMap[String, String]): Unit = {
+ def read_props(props: List[String], tab: HashMap[String, String])
+ {
props match {
case Nil => ()
case _ :: Nil => err()
@@ -112,8 +113,8 @@
}
}
- if (!empty_pattern.matcher(line).matches) {
- blank_pattern.split(line).toList match {
+ if (!empty_pattern.matcher(decl).matches) {
+ blank_pattern.split(decl).toList match {
case Nil => err()
case symbol :: props => {
val tab = new HashMap[String, String]
@@ -124,13 +125,6 @@
}
}
- private def read_symbols(path: String) = {
- val file = new File(isabelle_system.platform_path(path))
- if (file.canRead) {
- for (line <- Source.fromFile(file).getLines) read_line(line)
- }
- }
-
/* init tables */
@@ -154,9 +148,7 @@
/* constructor */
- read_symbols("$ISABELLE_HOME/etc/symbols")
- read_symbols("$ISABELLE_HOME_USER/etc/symbols")
+ symbol_decls.foreach(read_decl)
init_recoders()
}
-
}
--- a/src/Pure/General/yxml.scala Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/General/yxml.scala Wed Jan 21 16:51:45 2009 +0100
@@ -59,7 +59,7 @@
val s = source.toString
val i = s.indexOf('=')
if (i <= 0) err_attribute()
- (s.substring(0, i), s.substring(i + 1))
+ (s.substring(0, i).intern, s.substring(i + 1))
}
@@ -91,7 +91,7 @@
if (chunk == Y_string) pop()
else {
chunks(Y, chunk).toList match {
- case "" :: name :: atts => push(name.toString, atts.map(parse_attrib))
+ case "" :: name :: atts => push(name.toString.intern, atts.map(parse_attrib))
case txts => for (txt <- txts) add(XML.Text(txt.toString))
}
}
--- a/src/Pure/ML-Systems/alice.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/alice.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/alice.ML
- ID: $Id$
Compatibility file for Alice 1.4.
--- a/src/Pure/ML-Systems/exn.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/exn.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/exn.ML
- ID: $Id$
Author: Makarius
Extra support for exceptions.
--- a/src/Pure/ML-Systems/install_pp_polyml.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/install_pp_polyml.ML
- ID: $Id$
Extra toplevel pretty-printing for Poly/ML.
*)
--- a/src/Pure/ML-Systems/ml_name_space.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/ml_name_space.ML
- ID: $Id$
Author: Makarius
ML name space -- dummy version of Poly/ML 5.2 facility.
--- a/src/Pure/ML-Systems/multithreading.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/multithreading.ML
- ID: $Id$
Author: Makarius
Dummy implementation of multithreading setup.
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/multithreading_polyml.ML
- ID: $Id$
Author: Makarius
Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml).
--- a/src/Pure/ML-Systems/overloading_smlnj.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/overloading_smlnj.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/overloading_smlnj.ML
- ID: $Id$
Author: Makarius
Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml-4.1.3.ML
- ID: $Id$
Compatibility wrapper for Poly/ML 4.1.3.
*)
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml-4.1.4.ML
- ID: $Id$
Compatibility wrapper for Poly/ML 4.1.4.
*)
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml-4.2.0.ML
- ID: $Id$
Compatibility wrapper for Poly/ML 4.2.0.
*)
--- a/src/Pure/ML-Systems/polyml-5.0.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml-5.0.ML
- ID: $Id$
Compatibility wrapper for Poly/ML 5.0.
*)
--- a/src/Pure/ML-Systems/polyml-5.1.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml-5.1.ML
- ID: $Id$
Compatibility wrapper for Poly/ML 5.1.
*)
--- a/src/Pure/ML-Systems/polyml.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml.ML
- ID: $Id$
Compatibility wrapper for Poly/ML 5.2 or later.
*)
--- a/src/Pure/ML-Systems/polyml_common.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml_common.ML
- ID: $Id$
Compatibility file for Poly/ML -- common part for 4.x and 5.x.
*)
--- a/src/Pure/ML-Systems/polyml_old_basis.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_basis.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml_old_basis.ML
- ID: $Id$
Fixes for the old SML basis library (before Poly/ML 4.2.0).
*)
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml_old_compiler4.ML
- ID: $Id$
Runtime compilation -- for old PolyML.compiler (version 4.x).
*)
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/polyml_old_compiler5.ML
- ID: $Id$
Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
*)
--- a/src/Pure/ML-Systems/proper_int.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/proper_int.ML
- ID: $Id$
Author: Makarius
SML basis with type int representing proper integers, not machine
--- a/src/Pure/ML-Systems/smlnj.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/smlnj.ML
- ID: $Id$
Compatibility file for Standard ML of New Jersey 110 or later.
*)
--- a/src/Pure/ML-Systems/system_shell.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/system_shell.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/system_shell.ML
- ID: $Id$
Author: Makarius
Generic system shell processes (no provisions to propagate interrupts;
--- a/src/Pure/ML-Systems/thread_dummy.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/thread_dummy.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/thread_dummy.ML
- ID: $Id$
Author: Makarius
Default (mostly dummy) implementation of thread structures
--- a/src/Pure/ML-Systems/time_limit.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/time_limit.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/time_limit.ML
- ID: $Id$
Author: Makarius
Dummy implementation of NJ's TimeLimit structure.
--- a/src/Pure/ML-Systems/universal.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/ML-Systems/universal.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ML-Systems/universal.ML
- ID: $Id$
Author: Makarius
Universal values via tagged union. Emulates structure Universal
--- a/src/Pure/Syntax/ast.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/ast.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/ast.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Abstract syntax trees, translation rules, matching and normalization of asts.
--- a/src/Pure/Syntax/lexicon.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/lexicon.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/lexicon.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Lexer for the inner Isabelle syntax (terms and types).
--- a/src/Pure/Syntax/mixfix.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/mixfix.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Mixfix declarations, infixes, binders.
--- a/src/Pure/Syntax/parser.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/parser.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/parser.ML
- ID: $Id$
Author: Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen
General context-free parser for the inner syntax of terms, types, etc.
--- a/src/Pure/Syntax/printer.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/printer.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/printer.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Pretty printing of asts, terms, types and print (ast) translation.
--- a/src/Pure/Syntax/simple_syntax.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/simple_syntax.ML
- ID: $Id$
Author: Makarius
Simple syntax for types and terms --- for bootstrapping Pure.
--- a/src/Pure/Syntax/syn_ext.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/syn_ext.ML
- ID: $Id$
Author: Markus Wenzel and Carsten Clasohm, TU Muenchen
Syntax extension (internal interface).
--- a/src/Pure/Syntax/type_ext.ML Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Syntax/type_ext.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/type_ext.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Utilities for input and output of types. Also the concrete syntax of
--- a/src/Pure/Tools/isabelle_process.scala Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.scala Wed Jan 21 16:51:45 2009 +0100
@@ -7,7 +7,6 @@
package isabelle
-import java.util.Properties
import java.util.concurrent.LinkedBlockingQueue
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
InputStream, OutputStream, IOException}
@@ -80,23 +79,27 @@
kind == STATUS
}
- class Result(val kind: Kind.Value, val props: Properties, val result: String) {
+ class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
override def toString = {
val trees = YXML.parse_body_failsafe(result)
val res =
if (kind == Kind.STATUS) trees.map(_.toString).mkString
else trees.flatMap(XML.content(_).mkString).mkString
- if (props == null) kind.toString + " [[" + res + "]]"
- else kind.toString + " " + props.toString + " [[" + res + "]]"
+ if (props.isEmpty)
+ kind.toString + " [[" + res + "]]"
+ else
+ kind.toString + " " +
+ (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
}
def is_raw = Kind.is_raw(kind)
def is_control = Kind.is_control(kind)
def is_system = Kind.is_system(kind)
}
- def parse_message(kind: Kind.Value, result: String) = {
- XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))),
- YXML.parse_body_failsafe(result))
+ def parse_message(isabelle_system: IsabelleSystem, result: Result) =
+ {
+ XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
+ YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
}
}
@@ -119,17 +122,22 @@
private var closing = false
private var pid: String = null
private var the_session: String = null
- def session() = the_session
+ def session = the_session
/* results */
+ def parse_message(result: Result): XML.Tree =
+ IsabelleProcess.parse_message(isabelle_system, result)
+
private val result_queue = new LinkedBlockingQueue[Result]
- private def put_result(kind: Kind.Value, props: Properties, result: String) {
- if (kind == Kind.INIT && props != null) {
- pid = props.getProperty(Markup.PID)
- the_session = props.getProperty(Markup.SESSION)
+ private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
+ {
+ if (kind == Kind.INIT) {
+ val map = Map(props: _*)
+ if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
+ if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
}
result_queue.put(new Result(kind, props, result))
}
@@ -143,7 +151,7 @@
catch { case _: NullPointerException => null }
if (result != null) {
- results.event(result) // FIXME try/catch (!??)
+ results.event(result)
if (result.kind == Kind.EXIT) finished = true
}
else finished = true
@@ -156,13 +164,13 @@
def interrupt() = synchronized {
if (proc == null) error("Cannot interrupt Isabelle: no process")
- if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
+ if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
else {
try {
if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
- put_result(Kind.SIGNAL, null, "INT")
+ put_result(Kind.SIGNAL, Nil, "INT")
else
- put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
+ put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
}
catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
}
@@ -173,7 +181,7 @@
else {
try_close()
Thread.sleep(500)
- put_result(Kind.SIGNAL, null, "KILL")
+ put_result(Kind.SIGNAL, Nil, "KILL")
proc.destroy
proc = null
pid = null
@@ -198,7 +206,7 @@
def command(text: String) =
output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
- def command(props: Properties, text: String) =
+ def command(props: List[(String, String)], text: String) =
output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
IsabelleSyntax.encode_string(text))
@@ -233,17 +241,17 @@
finished = true
}
else {
- put_result(Kind.STDIN, null, s)
+ put_result(Kind.STDIN, Nil, s)
writer.write(s)
writer.flush
}
//}}}
}
catch {
- case e: IOException => put_result(Kind.SYSTEM, null, "Stdin thread: " + e.getMessage)
+ case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
}
}
- put_result(Kind.SYSTEM, null, "Stdin thread terminated")
+ put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
}
}
@@ -267,7 +275,7 @@
else done = true
}
if (result.length > 0) {
- put_result(Kind.STDOUT, null, result.toString)
+ put_result(Kind.STDOUT, Nil, result.toString)
result.length = 0
}
else {
@@ -278,10 +286,10 @@
//}}}
}
catch {
- case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage)
+ case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
}
}
- put_result(Kind.SYSTEM, null, "Stdout thread terminated")
+ put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
}
}
@@ -292,7 +300,7 @@
override def run() = {
val reader = isabelle_system.fifo_reader(fifo)
var kind: Kind.Value = null
- var props: Properties = null
+ var props: List[(String, String)] = Nil
var result = new StringBuilder
var finished = false
@@ -307,7 +315,7 @@
} while (c >= 0 && c != 2)
if (result.length > 0) {
- put_result(Kind.SYSTEM, null, "Malformed message:\n" + result.toString)
+ put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
result.length = 0
}
if (c < 0) {
@@ -319,7 +327,6 @@
c = reader.read
if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
else kind = null
- props = null
}
//}}}
}
@@ -339,16 +346,16 @@
if (i > 0) {
val name = line.substring(0, i)
val value = line.substring(i + 1, len - 2)
- if (props == null) props = new Properties
- if (!props.containsKey(name)) props.setProperty(name, value)
+ props = (name, value) :: props
}
}
// last text line
else if (line.endsWith("\u0002.")) {
result.append(line.substring(0, len - 2))
- put_result(kind, props, result.toString)
+ put_result(kind, props.reverse, result.toString)
+ kind = null
+ props = Nil
result.length = 0
- kind = null
}
// text line
else {
@@ -360,10 +367,10 @@
}
}
catch {
- case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage)
+ case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
}
}
- put_result(Kind.SYSTEM, null, "Message thread terminated")
+ put_result(Kind.SYSTEM, Nil, "Message thread terminated")
}
}
@@ -377,7 +384,7 @@
{
val (msg, rc) = isabelle_system.isabelle_tool("version")
if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
- put_result(Kind.SYSTEM, null, msg)
+ put_result(Kind.SYSTEM, Nil, msg)
}
@@ -418,8 +425,8 @@
override def run() = {
val rc = proc.waitFor()
Thread.sleep(300)
- put_result(Kind.SYSTEM, null, "Exit thread terminated")
- put_result(Kind.EXIT, null, Integer.toString(rc))
+ put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
+ put_result(Kind.EXIT, Nil, Integer.toString(rc))
rm_fifo()
}
}.start
--- a/src/Pure/Tools/isabelle_syntax.scala Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Tools/isabelle_syntax.scala Wed Jan 21 16:51:45 2009 +0100
@@ -6,8 +6,6 @@
package isabelle
-import java.util.{Properties, Enumeration}
-
object IsabelleSyntax {
@@ -30,7 +28,7 @@
def encode_string(str: String) =
{
- val result = new StringBuilder(str.length + 20)
+ val result = new StringBuilder(str.length + 10)
append_string(str, result)
result.toString
}
@@ -53,7 +51,7 @@
def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
{
- val result = new StringBuilder(20)
+ val result = new StringBuilder
append_list(append_elem, elems, result)
result.toString
}
@@ -61,22 +59,16 @@
/* properties */
- def append_properties(props: Properties, result: StringBuilder)
+ def append_properties(props: List[(String, String)], result: StringBuilder)
{
- result.append("(")
- val names = props.propertyNames.asInstanceOf[Enumeration[String]]
- while (names.hasMoreElements) {
- val name = names.nextElement; val value = props.getProperty(name)
- append_string(name, result); result.append(" = "); append_string(value, result)
- if (names.hasMoreElements) result.append(", ")
- }
- result.append(")")
+ append_list((p: (String, String), res) =>
+ { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
}
- def encode_properties(props: Properties) = {
- val result = new StringBuilder(40)
+ def encode_properties(props: List[(String, String)]) =
+ {
+ val result = new StringBuilder
append_properties(props, result)
result.toString
}
-
}
--- a/src/Pure/Tools/isabelle_system.scala Wed Jan 21 16:50:09 2009 +0100
+++ b/src/Pure/Tools/isabelle_system.scala Wed Jan 21 16:51:45 2009 +0100
@@ -143,4 +143,16 @@
}
logics.toList.sort(_ < _)
}
+
+
+ /* symbols */
+
+ private def read_symbols(path: String) = {
+ val file = new File(platform_path(path))
+ if (file.canRead) Source.fromFile(file).getLines
+ else Iterator.empty
+ }
+ val symbols = new Symbol.Interpretation(
+ read_symbols("$ISABELLE_HOME/etc/symbols") ++
+ read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
}