# HG changeset patch # User haftmann # Date 1232553105 -3600 # Node ID 88ba5e5ac6d84c35e67493f39cca8e16f0bc5235 # Parent bb0f395db245581e0e24c8bfd6122e63fbe31347# Parent 1f930609dcd096713fe7b364506dd9d25aba2f07 merged diff -r 1f930609dcd0 -r 88ba5e5ac6d8 doc-src/Locales/Locales/Examples.thy --- 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 \ lattice diff -r 1f930609dcd0 -r 88ba5e5ac6d8 doc-src/Locales/Locales/Examples3.thy --- 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 \ nat \ nat \ 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 \ nat \ 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 "\" 50) + + le: partial_order + le': partial_order le' for le' (infixl "\" 50) + fixes \ :: "'a \ 'b" assumes hom_le: "x \ y \ \ x \ \ 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 \} and @{text \}. How can one refer to a theorem for a particular order, @{text \} or @{text \}? 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 \} 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 \}! This can, of course, not be introduced automatically, but it can be declared manually through an abbreviation. *} @@ -321,7 +315,7 @@ less' (infixl "\" 50) where "less' \ 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 \} is a lattice homomorphism if it preserves meet and join. *} - locale lattice_hom = lattice + lat'!: lattice le' for le' (infixl "\" 50) + + locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\" 50) + fixes \ assumes hom_meet: "\ (lattice.meet le x y) = lattice.meet le' (\ x) (\ y)" @@ -341,9 +335,9 @@ "\ (lattice.join le x y) = lattice.join le' (\ x) (\ y)" abbreviation (in lattice_hom) - meet' (infixl "\''" 50) where "meet' \ lat'.meet" + meet' (infixl "\''" 50) where "meet' \ le'.meet" abbreviation (in lattice_hom) - join' (infixl "\''" 50) where "join' \ lat'.join" + join' (infixl "\''" 50) where "join' \ le'.join" text {* A homomorphism is an endomorphism if both orders coincide. *} @@ -400,17 +394,17 @@ sublocale lattice_hom \ order_preserving proof unfold_locales fix x y assume "x \ y" - then have "y = (x \ y)" by (simp add: join_connection) + then have "y = (x \ y)" by (simp add: le.join_connection) then have "\ y = (\ x \' \ y)" by (simp add: hom_join [symmetric]) - then show "\ x \ \ y" by (simp add: lat'.join_connection) + then show "\ x \ \ 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} *} diff -r 1f930609dcd0 -r 88ba5e5ac6d8 doc-src/Locales/Locales/ROOT.ML --- 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"; diff -r 1f930609dcd0 -r 88ba5e5ac6d8 doc-src/Locales/Locales/document/Examples.tex --- 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% % diff -r 1f930609dcd0 -r 88ba5e5ac6d8 doc-src/Locales/Locales/document/Examples3.tex --- 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}% diff -r 1f930609dcd0 -r 88ba5e5ac6d8 doc-src/Locales/Locales/document/root.tex --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Concurrent/mailbox.ML --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Concurrent/simple_thread.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Concurrent/synchronized.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/General/symbol.scala --- 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() } - } diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/General/yxml.scala --- 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)) } } diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/alice.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/exn.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/install_pp_polyml.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/ml_name_space.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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/multithreading.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/multithreading_polyml.ML --- 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). diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/overloading_smlnj.ML --- 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). diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml-4.1.3.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml-4.1.4.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml-4.2.0.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml-5.0.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml-5.1.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml_common.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml_old_basis.ML --- 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). *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml_old_compiler4.ML --- 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). *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/polyml_old_compiler5.ML --- 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). *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/proper_int.ML --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/smlnj.ML --- 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. *) diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/system_shell.ML --- 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; diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/thread_dummy.ML --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/time_limit.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/ML-Systems/universal.ML --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/ast.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/lexicon.ML --- 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). diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/mixfix.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/parser.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/printer.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/simple_syntax.ML --- 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. diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/syn_ext.ML --- 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). diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Syntax/type_ext.ML --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Tools/isabelle_process.scala --- 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 diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Tools/isabelle_syntax.scala --- 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 } - } diff -r 1f930609dcd0 -r 88ba5e5ac6d8 src/Pure/Tools/isabelle_system.scala --- 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")) }