# HG changeset patch
# User wenzelm
# Date 1393783245 -3600
# Node ID 154855d9a56483b7ba8d869087c1665044a73e92
# Parent  eb8e231a335fe136c88f14717609911cfd143b1e
clarified names of antiquotations and markup;
more documentation;

diff -r eb8e231a335f -r 154855d9a564 src/Doc/IsarImplementation/Logic.thy
--- 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}.
 
diff -r eb8e231a335f -r 154855d9a564 src/Doc/IsarImplementation/ML.thy
--- 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"}.  *}
 
diff -r eb8e231a335f -r 154855d9a564 src/Doc/IsarImplementation/Prelim.thy
--- 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}).
diff -r eb8e231a335f -r 154855d9a564 src/Doc/IsarRef/Document_Preparation.thy
--- 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.
diff -r eb8e231a335f -r 154855d9a564 src/Doc/IsarRef/Proof.thy
--- 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
diff -r eb8e231a335f -r 154855d9a564 src/Doc/IsarRef/Spec.thy
--- 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
diff -r eb8e231a335f -r 154855d9a564 src/Doc/LaTeXsugar/Sugar.thy
--- 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}
diff -r eb8e231a335f -r 154855d9a564 src/Doc/antiquote_setup.ML
--- 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;
diff -r eb8e231a335f -r 154855d9a564 src/HOL/ex/ML.thy
--- 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)) *}
diff -r eb8e231a335f -r 154855d9a564 src/Pure/ML/ml_compiler_polyml.ML
--- 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
diff -r eb8e231a335f -r 154855d9a564 src/Pure/PIDE/markup.ML
--- 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";
 
 
diff -r eb8e231a335f -r 154855d9a564 src/Pure/PIDE/markup.scala
--- 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"
 
 
diff -r eb8e231a335f -r 154855d9a564 src/Pure/Thy/thy_output.ML
--- 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 (!?) *)
diff -r eb8e231a335f -r 154855d9a564 src/Tools/jEdit/src/rendering.scala
--- 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 =