--- a/src/Doc/IsarImplementation/Logic.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy Sun Mar 02 19:00:45 2014 +0100
@@ -696,7 +696,7 @@
abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the
same inference kernel that is mainly responsible for @{ML_type thm}.
Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
- are located in the @{ML_struct Thm} module, even though theorems are
+ are located in the @{ML_structure Thm} module, even though theorems are
not yet involved at that stage.
\item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
@@ -717,7 +717,7 @@
\item Type @{ML_type thm} represents proven propositions. This is
an abstract datatype that guarantees that its values have been
- constructed by basic principles of the @{ML_struct Thm} module.
+ constructed by basic principles of the @{ML_structure Thm} module.
Every @{ML_type thm} value refers its background theory,
cf.\ \secref{sec:context-theory}.
--- a/src/Doc/IsarImplementation/ML.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Sun Mar 02 19:00:45 2014 +0100
@@ -1439,8 +1439,8 @@
Literal integers in ML text are forced to be of this one true
integer type --- adhoc overloading of SML97 is disabled.
- Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
- @{ML_struct Int}. Structure @{ML_struct Integer} in @{file
+ Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
+ @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
"~~/src/Pure/General/integer.ML"} provides some additional
operations.
@@ -1487,7 +1487,7 @@
*}
text {* Apart from @{ML Option.map} most other operations defined in
- structure @{ML_struct Option} are alien to Isabelle/ML an never
+ structure @{ML_structure Option} are alien to Isabelle/ML an never
used. The operations shown above are defined in @{file
"~~/src/Pure/General/basics.ML"}. *}
--- a/src/Doc/IsarImplementation/Prelim.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy Sun Mar 02 19:00:45 2014 +0100
@@ -709,7 +709,7 @@
of declared type and term variable names. Projecting a proof
context down to a primitive name context is occasionally useful when
invoking lower-level operations. Regular management of ``fresh
- variables'' is done by suitable operations of structure @{ML_struct
+ variables'' is done by suitable operations of structure @{ML_structure
Variable}, which is also able to provide an official status of
``locally fixed variable'' within the logical environment (cf.\
\secref{sec:variables}).
--- a/src/Doc/IsarRef/Document_Preparation.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Sun Mar 02 19:00:45 2014 +0100
@@ -123,7 +123,8 @@
@{antiquotation_def ML} & : & @{text antiquotation} \\
@{antiquotation_def ML_op} & : & @{text antiquotation} \\
@{antiquotation_def ML_type} & : & @{text antiquotation} \\
- @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
@{antiquotation_def "file"} & : & @{text antiquotation} \\
@{antiquotation_def "url"} & : & @{text antiquotation} \\
\end{matharray}
@@ -175,7 +176,8 @@
@@{antiquotation ML} options @{syntax name} |
@@{antiquotation ML_op} options @{syntax name} |
@@{antiquotation ML_type} options @{syntax name} |
- @@{antiquotation ML_struct} options @{syntax name} |
+ @@{antiquotation ML_structure} options @{syntax name} |
+ @@{antiquotation ML_functor} options @{syntax name} |
@@{antiquotation "file"} options @{syntax name} |
@@{antiquotation file_unchecked} options @{syntax name} |
@@{antiquotation url} options @{syntax name}
@@ -263,9 +265,9 @@
``@{text _}'' placeholders there.
\item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type
- s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value,
- infix operator, type, and structure, respectively. The source is
- printed verbatim.
+ s}"}, @{text "@{ML_structure s}"}, and @{text "@{ML_functor s}"}
+ check text @{text s} as ML value, infix operator, type, structure,
+ and functor respectively. The source is printed verbatim.
\item @{text "@{file path}"} checks that @{text "path"} refers to a
file (or directory) and prints it verbatim.
--- a/src/Doc/IsarRef/Proof.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy Sun Mar 02 19:00:45 2014 +0100
@@ -926,7 +926,7 @@
defines a proof method in the current theory. The given @{text
"text"} has to be an ML expression of type
@{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
- basic parsers defined in structure @{ML_struct Args} and @{ML_struct
+ basic parsers defined in structure @{ML_structure Args} and @{ML_structure
Attrib}. There are also combinators like @{ML METHOD} and @{ML
SIMPLE_METHOD} to turn certain tactic forms into official proof
methods; the primed versions refer to tactics with explicit goal
--- a/src/Doc/IsarRef/Spec.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy Sun Mar 02 19:00:45 2014 +0100
@@ -1059,7 +1059,7 @@
defines an attribute in the current theory. The given @{text
"text"} has to be an ML expression of type
@{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
- structure @{ML_struct Args} and @{ML_struct Attrib}.
+ structure @{ML_structure Args} and @{ML_structure Attrib}.
In principle, attributes can operate both on a given theorem and the
implicit context, although in practice only one is modified and the
--- a/src/Doc/LaTeXsugar/Sugar.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/LaTeXsugar/Sugar.thy Sun Mar 02 19:00:45 2014 +0100
@@ -398,7 +398,7 @@
Further use cases can be found in \S\ref{sec:yourself}.
If you are not afraid of ML, you may also define your own styles.
-Have a look at module @{ML_struct Term_Style}.
+Have a look at module @{ML_structure Term_Style}.
\section {Proofs}
--- a/src/Doc/antiquote_setup.ML Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Sun Mar 02 19:00:45 2014 +0100
@@ -64,8 +64,8 @@
ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
toks2 @ ml_toks ") option];";
-fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
- | ml_exn (toks1, toks2) =
+fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
+ | ml_exception (toks1, toks2) =
ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
fun ml_structure (toks, _) =
@@ -121,8 +121,8 @@
index_ml @{binding index_ML} "" ml_val #>
index_ml @{binding index_ML_op} "infix" ml_op #>
index_ml @{binding index_ML_type} "type" ml_type #>
- index_ml @{binding index_ML_exn} "exception" ml_exn #>
- index_ml @{binding index_ML_struct} "structure" ml_structure #>
+ index_ml @{binding index_ML_exception} "exception" ml_exception #>
+ index_ml @{binding index_ML_structure} "structure" ml_structure #>
index_ml @{binding index_ML_functor} "functor" ml_functor;
end;
--- a/src/HOL/ex/ML.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/HOL/ex/ML.thy Sun Mar 02 19:00:45 2014 +0100
@@ -104,7 +104,7 @@
*}
text {*
- The @{ML_struct Par_List} module provides high-level combinators for
+ The @{ML_structure Par_List} module provides high-level combinators for
parallel list operations. *}
ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
--- a/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 02 19:00:45 2014 +0100
@@ -64,7 +64,7 @@
| reported loc (PolyML.PTopenedAt decl) =
cons (reported_entity Markup.ML_openN loc decl)
| reported loc (PolyML.PTstructureAt decl) =
- cons (reported_entity Markup.ML_structN loc decl)
+ cons (reported_entity Markup.ML_structureN loc decl)
| reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
| reported _ _ = I
--- a/src/Pure/PIDE/markup.ML Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Mar 02 19:00:45 2014 +0100
@@ -92,7 +92,7 @@
val ML_commentN: string val ML_comment: T
val ML_defN: string
val ML_openN: string
- val ML_structN: string
+ val ML_structureN: string
val ML_typingN: string val ML_typing: T
val antiquotedN: string val antiquoted: T
val antiquoteN: string val antiquote: T
@@ -391,7 +391,7 @@
val ML_defN = "ML_def";
val ML_openN = "ML_open";
-val ML_structN = "ML_struct";
+val ML_structureN = "ML_structure";
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
--- a/src/Pure/PIDE/markup.scala Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Mar 02 19:00:45 2014 +0100
@@ -204,7 +204,7 @@
val ML_DEF = "ML_def"
val ML_OPEN = "ML_open"
- val ML_STRUCT = "ML_struct"
+ val ML_STRUCTURE = "ML_structure"
val ML_TYPING = "ML_typing"
--- a/src/Pure/Thy/thy_output.ML Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 02 19:00:45 2014 +0100
@@ -661,7 +661,7 @@
(ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text (Binding.name "ML_struct")
+ ml_text (Binding.name "ML_structure")
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
--- a/src/Tools/jEdit/src/rendering.scala Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sun Mar 02 19:00:45 2014 +0100
@@ -359,7 +359,7 @@
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
if !props.exists(
{ case (Markup.KIND, Markup.ML_OPEN) => true
- case (Markup.KIND, Markup.ML_STRUCT) => true
+ case (Markup.KIND, Markup.ML_STRUCTURE) => true
case _ => false }) =>
val opt_link =