clarified names of antiquotations and markup;
authorwenzelm
Sun Mar 02 19:00:45 2014 +0100 (2014-03-02)
changeset 55837154855d9a564
parent 55835 eb8e231a335f
child 55838 e120a15b0ee6
clarified names of antiquotations and markup;
more documentation;
src/Doc/IsarImplementation/Logic.thy
src/Doc/IsarImplementation/ML.thy
src/Doc/IsarImplementation/Prelim.thy
src/Doc/IsarRef/Document_Preparation.thy
src/Doc/IsarRef/Proof.thy
src/Doc/IsarRef/Spec.thy
src/Doc/LaTeXsugar/Sugar.thy
src/Doc/antiquote_setup.ML
src/HOL/ex/ML.thy
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Sun Mar 02 18:41:41 2014 +0100
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Sun Mar 02 19:00:45 2014 +0100
     1.3 @@ -696,7 +696,7 @@
     1.4    abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the
     1.5    same inference kernel that is mainly responsible for @{ML_type thm}.
     1.6    Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
     1.7 -  are located in the @{ML_struct Thm} module, even though theorems are
     1.8 +  are located in the @{ML_structure Thm} module, even though theorems are
     1.9    not yet involved at that stage.
    1.10  
    1.11    \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
    1.12 @@ -717,7 +717,7 @@
    1.13  
    1.14    \item Type @{ML_type thm} represents proven propositions.  This is
    1.15    an abstract datatype that guarantees that its values have been
    1.16 -  constructed by basic principles of the @{ML_struct Thm} module.
    1.17 +  constructed by basic principles of the @{ML_structure Thm} module.
    1.18    Every @{ML_type thm} value refers its background theory,
    1.19    cf.\ \secref{sec:context-theory}.
    1.20  
     2.1 --- a/src/Doc/IsarImplementation/ML.thy	Sun Mar 02 18:41:41 2014 +0100
     2.2 +++ b/src/Doc/IsarImplementation/ML.thy	Sun Mar 02 19:00:45 2014 +0100
     2.3 @@ -1439,8 +1439,8 @@
     2.4    Literal integers in ML text are forced to be of this one true
     2.5    integer type --- adhoc overloading of SML97 is disabled.
     2.6  
     2.7 -  Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
     2.8 -  @{ML_struct Int}.  Structure @{ML_struct Integer} in @{file
     2.9 +  Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
    2.10 +  @{ML_structure Int}.  Structure @{ML_structure Integer} in @{file
    2.11    "~~/src/Pure/General/integer.ML"} provides some additional
    2.12    operations.
    2.13  
    2.14 @@ -1487,7 +1487,7 @@
    2.15  *}
    2.16  
    2.17  text {* Apart from @{ML Option.map} most other operations defined in
    2.18 -  structure @{ML_struct Option} are alien to Isabelle/ML an never
    2.19 +  structure @{ML_structure Option} are alien to Isabelle/ML an never
    2.20    used.  The operations shown above are defined in @{file
    2.21    "~~/src/Pure/General/basics.ML"}.  *}
    2.22  
     3.1 --- a/src/Doc/IsarImplementation/Prelim.thy	Sun Mar 02 18:41:41 2014 +0100
     3.2 +++ b/src/Doc/IsarImplementation/Prelim.thy	Sun Mar 02 19:00:45 2014 +0100
     3.3 @@ -709,7 +709,7 @@
     3.4    of declared type and term variable names.  Projecting a proof
     3.5    context down to a primitive name context is occasionally useful when
     3.6    invoking lower-level operations.  Regular management of ``fresh
     3.7 -  variables'' is done by suitable operations of structure @{ML_struct
     3.8 +  variables'' is done by suitable operations of structure @{ML_structure
     3.9    Variable}, which is also able to provide an official status of
    3.10    ``locally fixed variable'' within the logical environment (cf.\
    3.11    \secref{sec:variables}).
     4.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Sun Mar 02 18:41:41 2014 +0100
     4.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Sun Mar 02 19:00:45 2014 +0100
     4.3 @@ -123,7 +123,8 @@
     4.4      @{antiquotation_def ML} & : & @{text antiquotation} \\
     4.5      @{antiquotation_def ML_op} & : & @{text antiquotation} \\
     4.6      @{antiquotation_def ML_type} & : & @{text antiquotation} \\
     4.7 -    @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
     4.8 +    @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
     4.9 +    @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
    4.10      @{antiquotation_def "file"} & : & @{text antiquotation} \\
    4.11      @{antiquotation_def "url"} & : & @{text antiquotation} \\
    4.12    \end{matharray}
    4.13 @@ -175,7 +176,8 @@
    4.14        @@{antiquotation ML} options @{syntax name} |
    4.15        @@{antiquotation ML_op} options @{syntax name} |
    4.16        @@{antiquotation ML_type} options @{syntax name} |
    4.17 -      @@{antiquotation ML_struct} options @{syntax name} |
    4.18 +      @@{antiquotation ML_structure} options @{syntax name} |
    4.19 +      @@{antiquotation ML_functor} options @{syntax name} |
    4.20        @@{antiquotation "file"} options @{syntax name} |
    4.21        @@{antiquotation file_unchecked} options @{syntax name} |
    4.22        @@{antiquotation url} options @{syntax name}
    4.23 @@ -263,9 +265,9 @@
    4.24    ``@{text _}'' placeholders there.
    4.25    
    4.26    \item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type
    4.27 -  s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value,
    4.28 -  infix operator, type, and structure, respectively.  The source is
    4.29 -  printed verbatim.
    4.30 +  s}"}, @{text "@{ML_structure s}"}, and @{text "@{ML_functor s}"}
    4.31 +  check text @{text s} as ML value, infix operator, type, structure,
    4.32 +  and functor respectively.  The source is printed verbatim.
    4.33  
    4.34    \item @{text "@{file path}"} checks that @{text "path"} refers to a
    4.35    file (or directory) and prints it verbatim.
     5.1 --- a/src/Doc/IsarRef/Proof.thy	Sun Mar 02 18:41:41 2014 +0100
     5.2 +++ b/src/Doc/IsarRef/Proof.thy	Sun Mar 02 19:00:45 2014 +0100
     5.3 @@ -926,7 +926,7 @@
     5.4    defines a proof method in the current theory.  The given @{text
     5.5    "text"} has to be an ML expression of type
     5.6    @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
     5.7 -  basic parsers defined in structure @{ML_struct Args} and @{ML_struct
     5.8 +  basic parsers defined in structure @{ML_structure Args} and @{ML_structure
     5.9    Attrib}.  There are also combinators like @{ML METHOD} and @{ML
    5.10    SIMPLE_METHOD} to turn certain tactic forms into official proof
    5.11    methods; the primed versions refer to tactics with explicit goal
     6.1 --- a/src/Doc/IsarRef/Spec.thy	Sun Mar 02 18:41:41 2014 +0100
     6.2 +++ b/src/Doc/IsarRef/Spec.thy	Sun Mar 02 19:00:45 2014 +0100
     6.3 @@ -1059,7 +1059,7 @@
     6.4    defines an attribute in the current theory.  The given @{text
     6.5    "text"} has to be an ML expression of type
     6.6    @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
     6.7 -  structure @{ML_struct Args} and @{ML_struct Attrib}.
     6.8 +  structure @{ML_structure Args} and @{ML_structure Attrib}.
     6.9  
    6.10    In principle, attributes can operate both on a given theorem and the
    6.11    implicit context, although in practice only one is modified and the
     7.1 --- a/src/Doc/LaTeXsugar/Sugar.thy	Sun Mar 02 18:41:41 2014 +0100
     7.2 +++ b/src/Doc/LaTeXsugar/Sugar.thy	Sun Mar 02 19:00:45 2014 +0100
     7.3 @@ -398,7 +398,7 @@
     7.4  
     7.5  Further use cases can be found in \S\ref{sec:yourself}.
     7.6  If you are not afraid of ML, you may also define your own styles.
     7.7 -Have a look at module @{ML_struct Term_Style}.
     7.8 +Have a look at module @{ML_structure Term_Style}.
     7.9  
    7.10  
    7.11  \section {Proofs}
     8.1 --- a/src/Doc/antiquote_setup.ML	Sun Mar 02 18:41:41 2014 +0100
     8.2 +++ b/src/Doc/antiquote_setup.ML	Sun Mar 02 19:00:45 2014 +0100
     8.3 @@ -64,8 +64,8 @@
     8.4        ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
     8.5          toks2 @ ml_toks ") option];";
     8.6  
     8.7 -fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
     8.8 -  | ml_exn (toks1, toks2) =
     8.9 +fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
    8.10 +  | ml_exception (toks1, toks2) =
    8.11        ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
    8.12  
    8.13  fun ml_structure (toks, _) =
    8.14 @@ -121,8 +121,8 @@
    8.15    index_ml @{binding index_ML} "" ml_val #>
    8.16    index_ml @{binding index_ML_op} "infix" ml_op #>
    8.17    index_ml @{binding index_ML_type} "type" ml_type #>
    8.18 -  index_ml @{binding index_ML_exn} "exception" ml_exn #>
    8.19 -  index_ml @{binding index_ML_struct} "structure" ml_structure #>
    8.20 +  index_ml @{binding index_ML_exception} "exception" ml_exception #>
    8.21 +  index_ml @{binding index_ML_structure} "structure" ml_structure #>
    8.22    index_ml @{binding index_ML_functor} "functor" ml_functor;
    8.23  
    8.24  end;
     9.1 --- a/src/HOL/ex/ML.thy	Sun Mar 02 18:41:41 2014 +0100
     9.2 +++ b/src/HOL/ex/ML.thy	Sun Mar 02 19:00:45 2014 +0100
     9.3 @@ -104,7 +104,7 @@
     9.4  *}
     9.5  
     9.6  text {*
     9.7 -  The @{ML_struct Par_List} module provides high-level combinators for
     9.8 +  The @{ML_structure Par_List} module provides high-level combinators for
     9.9    parallel list operations. *}
    9.10  
    9.11  ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
    10.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Sun Mar 02 18:41:41 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Sun Mar 02 19:00:45 2014 +0100
    10.3 @@ -64,7 +64,7 @@
    10.4        | reported loc (PolyML.PTopenedAt decl) =
    10.5            cons (reported_entity Markup.ML_openN loc decl)
    10.6        | reported loc (PolyML.PTstructureAt decl) =
    10.7 -          cons (reported_entity Markup.ML_structN loc decl)
    10.8 +          cons (reported_entity Markup.ML_structureN loc decl)
    10.9        | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   10.10        | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   10.11        | reported _ _ = I
    11.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 02 18:41:41 2014 +0100
    11.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 02 19:00:45 2014 +0100
    11.3 @@ -92,7 +92,7 @@
    11.4    val ML_commentN: string val ML_comment: T
    11.5    val ML_defN: string
    11.6    val ML_openN: string
    11.7 -  val ML_structN: string
    11.8 +  val ML_structureN: string
    11.9    val ML_typingN: string val ML_typing: T
   11.10    val antiquotedN: string val antiquoted: T
   11.11    val antiquoteN: string val antiquote: T
   11.12 @@ -391,7 +391,7 @@
   11.13  
   11.14  val ML_defN = "ML_def";
   11.15  val ML_openN = "ML_open";
   11.16 -val ML_structN = "ML_struct";
   11.17 +val ML_structureN = "ML_structure";
   11.18  val (ML_typingN, ML_typing) = markup_elem "ML_typing";
   11.19  
   11.20  
    12.1 --- a/src/Pure/PIDE/markup.scala	Sun Mar 02 18:41:41 2014 +0100
    12.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 02 19:00:45 2014 +0100
    12.3 @@ -204,7 +204,7 @@
    12.4  
    12.5    val ML_DEF = "ML_def"
    12.6    val ML_OPEN = "ML_open"
    12.7 -  val ML_STRUCT = "ML_struct"
    12.8 +  val ML_STRUCTURE = "ML_structure"
    12.9    val ML_TYPING = "ML_typing"
   12.10  
   12.11  
    13.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 02 18:41:41 2014 +0100
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 02 19:00:45 2014 +0100
    13.3 @@ -661,7 +661,7 @@
    13.4   (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
    13.5    ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
    13.6    ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
    13.7 -  ml_text (Binding.name "ML_struct")
    13.8 +  ml_text (Binding.name "ML_structure")
    13.9      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
   13.10  
   13.11    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
    14.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Mar 02 18:41:41 2014 +0100
    14.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Mar 02 19:00:45 2014 +0100
    14.3 @@ -359,7 +359,7 @@
    14.4            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    14.5            if !props.exists(
    14.6              { case (Markup.KIND, Markup.ML_OPEN) => true
    14.7 -              case (Markup.KIND, Markup.ML_STRUCT) => true
    14.8 +              case (Markup.KIND, Markup.ML_STRUCTURE) => true
    14.9                case _ => false }) =>
   14.10  
   14.11              val opt_link =