merged
authorwenzelm
Wed Jan 22 17:14:27 2014 +0100 (2014-01-22)
changeset 551140ee5c17f2207
parent 55102 761e40ce91bc
parent 55113 497693486858
child 55115 fbf24a326206
merged
NEWS
src/Doc/Datatypes/Datatypes.thy
src/HOL/Library/LaTeXsugar.thy
     1.1 --- a/NEWS	Wed Jan 22 10:13:40 2014 +0100
     1.2 +++ b/NEWS	Wed Jan 22 17:14:27 2014 +0100
     1.3 @@ -43,6 +43,10 @@
     1.4  context discipline.  See also Assumption.add_assumes and the more
     1.5  primitive Thm.assume_hyps.
     1.6  
     1.7 +* Inner syntax token language allows regular quoted strings "..."
     1.8 +(only makes sense in practice, if outer syntax is delimited
     1.9 +differently).
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     2.1 --- a/etc/isar-keywords.el	Wed Jan 22 10:13:40 2014 +0100
     2.2 +++ b/etc/isar-keywords.el	Wed Jan 22 17:14:27 2014 +0100
     2.3 @@ -272,8 +272,10 @@
     2.4      "syntax"
     2.5      "syntax_declaration"
     2.6      "term"
     2.7 +    "term_cartouche"
     2.8      "termination"
     2.9      "text"
    2.10 +    "text_cartouche"
    2.11      "text_raw"
    2.12      "then"
    2.13      "theorem"
    2.14 @@ -453,6 +455,7 @@
    2.15      "solve_direct"
    2.16      "spark_status"
    2.17      "term"
    2.18 +    "term_cartouche"
    2.19      "thm"
    2.20      "thm_deps"
    2.21      "thy_deps"
    2.22 @@ -591,6 +594,7 @@
    2.23      "syntax"
    2.24      "syntax_declaration"
    2.25      "text"
    2.26 +    "text_cartouche"
    2.27      "text_raw"
    2.28      "theorems"
    2.29      "translations"
     3.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Jan 22 10:13:40 2014 +0100
     3.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jan 22 17:14:27 2014 +0100
     3.3 @@ -451,12 +451,12 @@
     3.4    @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
     3.5  \end{matharray}
     3.6  
     3.7 -@{rail "
     3.8 +@{rail \<open>
     3.9    @@{command datatype_new} target? @{syntax dt_options}? \<newline>
    3.10      (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
    3.11    ;
    3.12    @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
    3.13 -"}
    3.14 +\<close>}
    3.15  
    3.16  The syntactic entity \synt{target} can be used to specify a local
    3.17  context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
    3.18 @@ -485,13 +485,13 @@
    3.19  The left-hand sides of the datatype equations specify the name of the type to
    3.20  define, its type parameters, and additional information:
    3.21  
    3.22 -@{rail "
    3.23 +@{rail \<open>
    3.24    @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
    3.25    ;
    3.26    @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
    3.27    ;
    3.28    @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
    3.29 -"}
    3.30 +\<close>}
    3.31  
    3.32  \noindent
    3.33  The syntactic entity \synt{name} denotes an identifier, \synt{typefree}
    3.34 @@ -504,10 +504,10 @@
    3.35  Inside a mutually recursive specification, all defined datatypes must
    3.36  mention exactly the same type variables in the same order.
    3.37  
    3.38 -@{rail "
    3.39 +@{rail \<open>
    3.40    @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \<newline>
    3.41      @{syntax dt_sel_defaults}? mixfix?
    3.42 -"}
    3.43 +\<close>}
    3.44  
    3.45  \medskip
    3.46  
    3.47 @@ -517,9 +517,9 @@
    3.48  can be supplied at the front to override the default name
    3.49  (@{text t.is_C\<^sub>j}).
    3.50  
    3.51 -@{rail "
    3.52 +@{rail \<open>
    3.53    @{syntax_def ctor_arg}: type | '(' name ':' type ')'
    3.54 -"}
    3.55 +\<close>}
    3.56  
    3.57  \medskip
    3.58  
    3.59 @@ -529,9 +529,9 @@
    3.60  (@{text un_C\<^sub>ji}). The same selector names can be reused for several
    3.61  constructors as long as they share the same type.
    3.62  
    3.63 -@{rail "
    3.64 +@{rail \<open>
    3.65    @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
    3.66 -"}
    3.67 +\<close>}
    3.68  
    3.69  \noindent
    3.70  Given a constructor
    3.71 @@ -552,9 +552,9 @@
    3.72    @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
    3.73  \end{matharray}
    3.74  
    3.75 -@{rail "
    3.76 +@{rail \<open>
    3.77    @@{command datatype_new_compat} names
    3.78 -"}
    3.79 +\<close>}
    3.80  
    3.81  \noindent
    3.82  The old datatype package provides some functionality that is not yet replicated
    3.83 @@ -1346,11 +1346,11 @@
    3.84    @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
    3.85  \end{matharray}
    3.86  
    3.87 -@{rail "
    3.88 +@{rail \<open>
    3.89    @@{command primrec_new} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
    3.90    ;
    3.91    @{syntax_def pr_equation}: thmdecl? prop
    3.92 -"}
    3.93 +\<close>}
    3.94  *}
    3.95  
    3.96  
    3.97 @@ -1568,10 +1568,10 @@
    3.98    @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
    3.99  \end{matharray}
   3.100  
   3.101 -@{rail "
   3.102 +@{rail \<open>
   3.103    @@{command codatatype} target? \<newline>
   3.104      (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   3.105 -"}
   3.106 +\<close>}
   3.107  
   3.108  \noindent
   3.109  Definitions of codatatypes have almost exactly the same syntax as for datatypes
   3.110 @@ -2235,7 +2235,7 @@
   3.111    @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
   3.112  \end{matharray}
   3.113  
   3.114 -@{rail "
   3.115 +@{rail \<open>
   3.116    (@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
   3.117      @{syntax pcr_option}? fixes @'where'
   3.118      (@{syntax pcr_formula} + '|')
   3.119 @@ -2243,7 +2243,7 @@
   3.120    @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
   3.121    ;
   3.122    @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
   3.123 -"}
   3.124 +\<close>}
   3.125  
   3.126  The optional target is potentially followed by a corecursion-specific option:
   3.127  
   3.128 @@ -2319,11 +2319,11 @@
   3.129    @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
   3.130  \end{matharray}
   3.131  
   3.132 -@{rail "
   3.133 +@{rail \<open>
   3.134    @@{command bnf} target? (name ':')? typ \<newline>
   3.135      'map:' term ('sets:' (term +))? 'bd:' term \<newline>
   3.136      ('wits:' (term +))? ('rel:' term)?
   3.137 -"}
   3.138 +\<close>}
   3.139  *}
   3.140  
   3.141  
   3.142 @@ -2336,7 +2336,7 @@
   3.143    @{text "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
   3.144  \end{matharray}
   3.145  
   3.146 -@{rail "
   3.147 +@{rail \<open>
   3.148    @@{command bnf_decl} target? @{syntax dt_name}
   3.149    ;
   3.150    @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
   3.151 @@ -2344,7 +2344,7 @@
   3.152    @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
   3.153    ;
   3.154    @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
   3.155 -"}
   3.156 +\<close>}
   3.157  
   3.158  Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
   3.159  and asserts the bnf properties for these constants as axioms. Additionally,
   3.160 @@ -2364,9 +2364,9 @@
   3.161    @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
   3.162  \end{matharray}
   3.163  
   3.164 -@{rail "
   3.165 +@{rail \<open>
   3.166    @@{command print_bnfs}
   3.167 -"}
   3.168 +\<close>}
   3.169  *}
   3.170  
   3.171  
   3.172 @@ -2410,7 +2410,7 @@
   3.173    @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
   3.174  \end{matharray}
   3.175  
   3.176 -@{rail "
   3.177 +@{rail \<open>
   3.178    @@{command wrap_free_constructors} target? @{syntax dt_options} \<newline>
   3.179      term_list name @{syntax wfc_discs_sels}?
   3.180    ;
   3.181 @@ -2419,7 +2419,7 @@
   3.182    @{syntax_def name_term}: (name ':' term)
   3.183    ;
   3.184    X_list: '[' (X + ',') ']'
   3.185 -"}
   3.186 +\<close>}
   3.187  
   3.188  % options: no_discs_sels no_code rep_compat
   3.189  
     4.1 --- a/src/Doc/IsarImplementation/Isar.thy	Wed Jan 22 10:13:40 2014 +0100
     4.2 +++ b/src/Doc/IsarImplementation/Isar.thy	Wed Jan 22 17:14:27 2014 +0100
     4.3 @@ -563,9 +563,9 @@
     4.4    @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\
     4.5    \end{matharray}
     4.6  
     4.7 -  @{rail "
     4.8 +  @{rail \<open>
     4.9    @@{ML_antiquotation attributes} attributes
    4.10 -  "}
    4.11 +  \<close>}
    4.12  
    4.13    \begin{description}
    4.14  
     5.1 --- a/src/Doc/IsarImplementation/Logic.thy	Wed Jan 22 10:13:40 2014 +0100
     5.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Wed Jan 22 17:14:27 2014 +0100
     5.3 @@ -196,7 +196,7 @@
     5.4    @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\
     5.5    \end{matharray}
     5.6  
     5.7 -  @{rail "
     5.8 +  @{rail \<open>
     5.9    @@{ML_antiquotation class} nameref
    5.10    ;
    5.11    @@{ML_antiquotation sort} sort
    5.12 @@ -206,7 +206,7 @@
    5.13     @@{ML_antiquotation nonterminal}) nameref
    5.14    ;
    5.15    @@{ML_antiquotation typ} type
    5.16 -  "}
    5.17 +  \<close>}
    5.18  
    5.19    \begin{description}
    5.20  
    5.21 @@ -444,7 +444,7 @@
    5.22    @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\
    5.23    \end{matharray}
    5.24  
    5.25 -  @{rail "
    5.26 +  @{rail \<open>
    5.27    (@@{ML_antiquotation const_name} |
    5.28     @@{ML_antiquotation const_abbrev}) nameref
    5.29    ;
    5.30 @@ -453,7 +453,7 @@
    5.31    @@{ML_antiquotation term} term
    5.32    ;
    5.33    @@{ML_antiquotation prop} prop
    5.34 -  "}
    5.35 +  \<close>}
    5.36  
    5.37    \begin{description}
    5.38  
    5.39 @@ -780,7 +780,7 @@
    5.40    @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
    5.41    \end{matharray}
    5.42  
    5.43 -  @{rail "
    5.44 +  @{rail \<open>
    5.45    @@{ML_antiquotation ctyp} typ
    5.46    ;
    5.47    @@{ML_antiquotation cterm} term
    5.48 @@ -793,7 +793,7 @@
    5.49    ;
    5.50    @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
    5.51      @'by' method method?
    5.52 -  "}
    5.53 +  \<close>}
    5.54  
    5.55    \begin{description}
    5.56  
     6.1 --- a/src/Doc/IsarImplementation/ML.thy	Wed Jan 22 10:13:40 2014 +0100
     6.2 +++ b/src/Doc/IsarImplementation/ML.thy	Wed Jan 22 17:14:27 2014 +0100
     6.3 @@ -666,9 +666,9 @@
     6.4    concept of \emph{ML antiquotation}.  The standard token language of
     6.5    ML is augmented by special syntactic entities of the following form:
     6.6  
     6.7 -  @{rail "
     6.8 +  @{rail \<open>
     6.9    @{syntax_def antiquote}: '@{' nameref args '}'
    6.10 -  "}
    6.11 +  \<close>}
    6.12  
    6.13    Here @{syntax nameref} and @{syntax args} are regular outer syntax
    6.14    categories \cite{isabelle-isar-ref}.  Attributes and proof methods
    6.15 @@ -699,9 +699,9 @@
    6.16    @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
    6.17    \end{matharray}
    6.18  
    6.19 -  @{rail "
    6.20 +  @{rail \<open>
    6.21    @@{ML_antiquotation make_string}
    6.22 -  "}
    6.23 +  \<close>}
    6.24  
    6.25    \begin{description}
    6.26  
     7.1 --- a/src/Doc/IsarImplementation/Prelim.thy	Wed Jan 22 10:13:40 2014 +0100
     7.2 +++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Jan 22 17:14:27 2014 +0100
     7.3 @@ -165,11 +165,11 @@
     7.4    @{ML_antiquotation_def "theory_context"} & : & @{text ML_antiquotation} \\
     7.5    \end{matharray}
     7.6  
     7.7 -  @{rail "
     7.8 +  @{rail \<open>
     7.9    @@{ML_antiquotation theory} nameref?
    7.10    ;
    7.11    @@{ML_antiquotation theory_context} nameref
    7.12 -  "}
    7.13 +  \<close>}
    7.14  
    7.15    \begin{description}
    7.16  
    7.17 @@ -1025,9 +1025,9 @@
    7.18    @{ML_antiquotation_def "binding"} & : & @{text ML_antiquotation} \\
    7.19    \end{matharray}
    7.20  
    7.21 -  @{rail "
    7.22 +  @{rail \<open>
    7.23    @@{ML_antiquotation binding} name
    7.24 -  "}
    7.25 +  \<close>}
    7.26  
    7.27    \begin{description}
    7.28  
     8.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 10:13:40 2014 +0100
     8.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 17:14:27 2014 +0100
     8.3 @@ -47,13 +47,13 @@
     8.4    markup commands, but have a different status within Isabelle/Isar
     8.5    syntax.
     8.6  
     8.7 -  @{rail "
     8.8 +  @{rail \<open>
     8.9      (@@{command chapter} | @@{command section} | @@{command subsection} |
    8.10        @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
    8.11      ;
    8.12      (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} |
    8.13        @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text}
    8.14 -  "}
    8.15 +  \<close>}
    8.16  
    8.17    \begin{description}
    8.18  
    8.19 @@ -148,7 +148,7 @@
    8.20    context.
    8.21  
    8.22    %% FIXME less monolithic presentation, move to individual sections!?
    8.23 -  @{rail "
    8.24 +  @{rail \<open>
    8.25      '@{' antiquotation '}'
    8.26      ;
    8.27      @{syntax_def antiquotation}:
    8.28 @@ -176,7 +176,7 @@
    8.29        @@{antiquotation ML_op} options @{syntax name} |
    8.30        @@{antiquotation ML_type} options @{syntax name} |
    8.31        @@{antiquotation ML_struct} options @{syntax name} |
    8.32 -      @@{antiquotation \"file\"} options @{syntax name} |
    8.33 +      @@{antiquotation "file"} options @{syntax name} |
    8.34        @@{antiquotation file_unchecked} options @{syntax name} |
    8.35        @@{antiquotation url} options @{syntax name}
    8.36      ;
    8.37 @@ -187,7 +187,7 @@
    8.38      styles: '(' (style + ',') ')'
    8.39      ;
    8.40      style: (@{syntax name} +)
    8.41 -  "}
    8.42 +  \<close>}
    8.43  
    8.44    Note that the syntax of antiquotations may \emph{not} include source
    8.45    comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
    8.46 @@ -404,11 +404,11 @@
    8.47    presentation tags, to indicate some modification in the way it is
    8.48    printed in the document.
    8.49  
    8.50 -  @{rail "
    8.51 +  @{rail \<open>
    8.52      @{syntax_def tags}: ( tag * )
    8.53      ;
    8.54      tag: '%' (@{syntax ident} | @{syntax string})
    8.55 -  "}
    8.56 +  \<close>}
    8.57  
    8.58    Some tags are pre-declared for certain classes of commands, serving
    8.59    as default markup if no tags are given in the text:
    8.60 @@ -457,7 +457,9 @@
    8.61      @{antiquotation_def "rail"} & : & @{text antiquotation} \\
    8.62    \end{matharray}
    8.63  
    8.64 -  @{rail "'rail' string"}
    8.65 +  @{rail \<open>
    8.66 +    'rail' (@{syntax string} | @{syntax cartouche})
    8.67 +  \<close>}
    8.68  
    8.69    The @{antiquotation rail} antiquotation allows to include syntax
    8.70    diagrams into Isabelle documents.  {\LaTeX} requires the style file
    8.71 @@ -468,7 +470,7 @@
    8.72    The rail specification language is quoted here as Isabelle @{syntax
    8.73    string}; it has its own grammar given below.
    8.74  
    8.75 -  @{rail "
    8.76 +  @{rail \<open>
    8.77    rule? + ';'
    8.78    ;
    8.79    rule: ((identifier | @{syntax antiquotation}) ':')? body
    8.80 @@ -479,13 +481,13 @@
    8.81    ;
    8.82    atom: '(' body? ')' | identifier |
    8.83      '@'? (string | @{syntax antiquotation}) |
    8.84 -    '\\\\\\\\'
    8.85 -  "}
    8.86 +    '\<newline>'
    8.87 +  \<close>}
    8.88  
    8.89    The lexical syntax of @{text "identifier"} coincides with that of
    8.90    @{syntax ident} in regular Isabelle syntax, but @{text string} uses
    8.91    single quotes instead of double quotes of the standard @{syntax
    8.92 -  string} category, to avoid extra escapes.
    8.93 +  string} category.
    8.94  
    8.95    Each @{text rule} defines a formal language (with optional name),
    8.96    using a notation that is similar to EBNF or regular expressions with
    8.97 @@ -496,62 +498,62 @@
    8.98  
    8.99    \item Empty @{verbatim "()"}
   8.100  
   8.101 -  @{rail "()"}
   8.102 +  @{rail \<open>()\<close>}
   8.103  
   8.104    \item Nonterminal @{verbatim "A"}
   8.105  
   8.106 -  @{rail "A"}
   8.107 +  @{rail \<open>A\<close>}
   8.108  
   8.109    \item Nonterminal via Isabelle antiquotation
   8.110    @{verbatim "@{syntax method}"}
   8.111  
   8.112 -  @{rail "@{syntax method}"}
   8.113 +  @{rail \<open>@{syntax method}\<close>}
   8.114  
   8.115    \item Terminal @{verbatim "'xyz'"}
   8.116  
   8.117 -  @{rail "'xyz'"}
   8.118 +  @{rail \<open>'xyz'\<close>}
   8.119  
   8.120    \item Terminal in keyword style @{verbatim "@'xyz'"}
   8.121  
   8.122 -  @{rail "@'xyz'"}
   8.123 +  @{rail \<open>@'xyz'\<close>}
   8.124  
   8.125    \item Terminal via Isabelle antiquotation
   8.126    @{verbatim "@@{method rule}"}
   8.127  
   8.128 -  @{rail "@@{method rule}"}
   8.129 +  @{rail \<open>@@{method rule}\<close>}
   8.130  
   8.131    \item Concatenation @{verbatim "A B C"}
   8.132  
   8.133 -  @{rail "A B C"}
   8.134 +  @{rail \<open>A B C\<close>}
   8.135  
   8.136    \item Newline inside concatenation
   8.137    @{verbatim "A B C \<newline> D E F"}
   8.138  
   8.139 -  @{rail "A B C \<newline> D E F"}
   8.140 +  @{rail \<open>A B C \<newline> D E F\<close>}
   8.141  
   8.142    \item Variants @{verbatim "A | B | C"}
   8.143  
   8.144 -  @{rail "A | B | C"}
   8.145 +  @{rail \<open>A | B | C\<close>}
   8.146  
   8.147    \item Option @{verbatim "A ?"}
   8.148  
   8.149 -  @{rail "A ?"}
   8.150 +  @{rail \<open>A ?\<close>}
   8.151  
   8.152    \item Repetition @{verbatim "A *"}
   8.153  
   8.154 -  @{rail "A *"}
   8.155 +  @{rail \<open>A *\<close>}
   8.156  
   8.157    \item Repetition with separator @{verbatim "A * sep"}
   8.158  
   8.159 -  @{rail "A * sep"}
   8.160 +  @{rail \<open>A * sep\<close>}
   8.161  
   8.162    \item Strict repetition @{verbatim "A +"}
   8.163  
   8.164 -  @{rail "A +"}
   8.165 +  @{rail \<open>A +\<close>}
   8.166  
   8.167    \item Strict repetition with separator @{verbatim "A + sep"}
   8.168  
   8.169 -  @{rail "A + sep"}
   8.170 +  @{rail \<open>A + sep\<close>}
   8.171  
   8.172    \end{itemize}
   8.173  *}
   8.174 @@ -564,10 +566,9 @@
   8.175      @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   8.176    \end{matharray}
   8.177  
   8.178 -  @{rail "
   8.179 +  @{rail \<open>
   8.180      @@{command display_drafts} (@{syntax name} +)
   8.181 -
   8.182 -  "}
   8.183 +  \<close>}
   8.184  
   8.185    \begin{description}
   8.186  
     9.1 --- a/src/Doc/IsarRef/Generic.thy	Wed Jan 22 10:13:40 2014 +0100
     9.2 +++ b/src/Doc/IsarRef/Generic.thy	Wed Jan 22 17:14:27 2014 +0100
     9.3 @@ -34,9 +34,9 @@
     9.4      @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
     9.5    \end{matharray}
     9.6  
     9.7 -  @{rail "
     9.8 +  @{rail \<open>
     9.9      @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
    9.10 -  "}
    9.11 +  \<close>}
    9.12  
    9.13    \begin{description}
    9.14    
    9.15 @@ -70,14 +70,14 @@
    9.16      @{method_def fail} & : & @{text method} \\
    9.17    \end{matharray}
    9.18  
    9.19 -  @{rail "
    9.20 +  @{rail \<open>
    9.21      (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
    9.22      ;
    9.23      (@@{method erule} | @@{method drule} | @@{method frule})
    9.24        ('(' @{syntax nat} ')')? @{syntax thmrefs}
    9.25      ;
    9.26      (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
    9.27 -  "}
    9.28 +  \<close>}
    9.29  
    9.30    \begin{description}
    9.31    
    9.32 @@ -136,7 +136,7 @@
    9.33      @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
    9.34    \end{matharray}
    9.35  
    9.36 -  @{rail "
    9.37 +  @{rail \<open>
    9.38      @@{attribute tagged} @{syntax name} @{syntax name}
    9.39      ;
    9.40      @@{attribute untagged} @{syntax name}
    9.41 @@ -146,7 +146,7 @@
    9.42      (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
    9.43      ;
    9.44      @@{attribute rotated} @{syntax int}?
    9.45 -  "}
    9.46 +  \<close>}
    9.47  
    9.48    \begin{description}
    9.49  
    9.50 @@ -201,11 +201,11 @@
    9.51      @{method_def split} & : & @{text method} \\
    9.52    \end{matharray}
    9.53  
    9.54 -  @{rail "
    9.55 +  @{rail \<open>
    9.56      @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
    9.57      ;
    9.58      @@{method split} @{syntax thmrefs}
    9.59 -  "}
    9.60 +  \<close>}
    9.61  
    9.62    These methods provide low-level facilities for equational reasoning
    9.63    that are intended for specialized applications only.  Normally,
    9.64 @@ -304,7 +304,7 @@
    9.65      @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
    9.66    \end{matharray}
    9.67  
    9.68 -  @{rail "
    9.69 +  @{rail \<open>
    9.70      (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
    9.71        @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
    9.72      ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
    9.73 @@ -319,7 +319,7 @@
    9.74      ;
    9.75  
    9.76      dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
    9.77 -  "}
    9.78 +  \<close>}
    9.79  
    9.80  \begin{description}
    9.81  
    9.82 @@ -406,7 +406,7 @@
    9.83      @{method_def simp_all} & : & @{text method} \\
    9.84    \end{matharray}
    9.85  
    9.86 -  @{rail "
    9.87 +  @{rail \<open>
    9.88      (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
    9.89      ;
    9.90  
    9.91 @@ -414,7 +414,7 @@
    9.92      ;
    9.93      @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
    9.94        'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
    9.95 -  "}
    9.96 +  \<close>}
    9.97  
    9.98    \begin{description}
    9.99  
   9.100 @@ -608,10 +608,10 @@
   9.101      @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   9.102    \end{matharray}
   9.103  
   9.104 -  @{rail "
   9.105 +  @{rail \<open>
   9.106      (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
   9.107        (() | 'add' | 'del')
   9.108 -  "}
   9.109 +  \<close>}
   9.110  
   9.111    \begin{description}
   9.112  
   9.113 @@ -923,13 +923,13 @@
   9.114      simproc & : & @{text attribute} \\
   9.115    \end{matharray}
   9.116  
   9.117 -  @{rail "
   9.118 +  @{rail \<open>
   9.119      @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
   9.120        @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
   9.121      ;
   9.122  
   9.123      @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   9.124 -  "}
   9.125 +  \<close>}
   9.126  
   9.127    \begin{description}
   9.128  
   9.129 @@ -1229,12 +1229,12 @@
   9.130      @{attribute_def simplified} & : & @{text attribute} \\
   9.131    \end{matharray}
   9.132  
   9.133 -  @{rail "
   9.134 +  @{rail \<open>
   9.135      @@{attribute simplified} opt? @{syntax thmrefs}?
   9.136      ;
   9.137  
   9.138      opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
   9.139 -  "}
   9.140 +  \<close>}
   9.141  
   9.142    \begin{description}
   9.143    
   9.144 @@ -1490,13 +1490,13 @@
   9.145      @{attribute_def swapped} & : & @{text attribute} \\
   9.146    \end{matharray}
   9.147  
   9.148 -  @{rail "
   9.149 +  @{rail \<open>
   9.150      (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
   9.151      ;
   9.152      @@{attribute rule} 'del'
   9.153      ;
   9.154      @@{attribute iff} (((() | 'add') '?'?) | 'del')
   9.155 -  "}
   9.156 +  \<close>}
   9.157  
   9.158    \begin{description}
   9.159  
   9.160 @@ -1562,9 +1562,9 @@
   9.161      @{method_def contradiction} & : & @{text method} \\
   9.162    \end{matharray}
   9.163  
   9.164 -  @{rail "
   9.165 +  @{rail \<open>
   9.166      @@{method rule} @{syntax thmrefs}?
   9.167 -  "}
   9.168 +  \<close>}
   9.169  
   9.170    \begin{description}
   9.171  
   9.172 @@ -1603,7 +1603,7 @@
   9.173      @{method_def deepen} & : & @{text method} \\
   9.174    \end{matharray}
   9.175  
   9.176 -  @{rail "
   9.177 +  @{rail \<open>
   9.178      @@{method blast} @{syntax nat}? (@{syntax clamod} * )
   9.179      ;
   9.180      @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
   9.181 @@ -1624,7 +1624,7 @@
   9.182        ('cong' | 'split') (() | 'add' | 'del') |
   9.183        'iff' (((() | 'add') '?'?) | 'del') |
   9.184        (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
   9.185 -  "}
   9.186 +  \<close>}
   9.187  
   9.188    \begin{description}
   9.189  
   9.190 @@ -1735,11 +1735,11 @@
   9.191      @{method_def clarsimp} & : & @{text method} \\
   9.192    \end{matharray}
   9.193  
   9.194 -  @{rail "
   9.195 +  @{rail \<open>
   9.196      (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
   9.197      ;
   9.198      @@{method clarsimp} (@{syntax clasimpmod} * )
   9.199 -  "}
   9.200 +  \<close>}
   9.201  
   9.202    \begin{description}
   9.203  
   9.204 @@ -1926,13 +1926,13 @@
   9.205    Generic tools may refer to the information provided by object-logic
   9.206    declarations internally.
   9.207  
   9.208 -  @{rail "
   9.209 +  @{rail \<open>
   9.210      @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
   9.211      ;
   9.212      @@{attribute atomize} ('(' 'full' ')')?
   9.213      ;
   9.214      @@{attribute rule_format} ('(' 'noasm' ')')?
   9.215 -  "}
   9.216 +  \<close>}
   9.217  
   9.218    \begin{description}
   9.219    
    10.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 22 10:13:40 2014 +0100
    10.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 22 17:14:27 2014 +0100
    10.3 @@ -96,17 +96,17 @@
    10.4    introduction rule.  The default rule declarations of Isabelle/HOL
    10.5    already take care of most common situations.
    10.6  
    10.7 -  @{rail "
    10.8 +  @{rail \<open>
    10.9      (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
   10.10        @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
   10.11      @{syntax target}? \<newline>
   10.12 -    @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \<newline>
   10.13 +    @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
   10.14      (@'monos' @{syntax thmrefs})?
   10.15      ;
   10.16      clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
   10.17      ;
   10.18      @@{attribute (HOL) mono} (() | 'add' | 'del')
   10.19 -  "}
   10.20 +  \<close>}
   10.21  
   10.22    \begin{description}
   10.23  
   10.24 @@ -264,11 +264,11 @@
   10.25      @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   10.26    \end{matharray}
   10.27  
   10.28 -  @{rail "
   10.29 -    @@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations
   10.30 +  @{rail \<open>
   10.31 +    @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
   10.32      ;
   10.33      (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
   10.34 -      @{syntax \"fixes\"} \<newline> @'where' equations
   10.35 +      @{syntax "fixes"} \<newline> @'where' equations
   10.36      ;
   10.37  
   10.38      equations: (@{syntax thmdecl}? @{syntax prop} + '|')
   10.39 @@ -278,7 +278,7 @@
   10.40      @@{command (HOL) termination} @{syntax term}?
   10.41      ;
   10.42      @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
   10.43 -  "}
   10.44 +  \<close>}
   10.45  
   10.46    \begin{description}
   10.47  
   10.48 @@ -508,7 +508,7 @@
   10.49      @{method_def (HOL) induction_schema} & : & @{text method} \\
   10.50    \end{matharray}
   10.51  
   10.52 -  @{rail "
   10.53 +  @{rail \<open>
   10.54      @@{method (HOL) relation} @{syntax term}
   10.55      ;
   10.56      @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
   10.57 @@ -518,7 +518,7 @@
   10.58      @@{method (HOL) induction_schema}
   10.59      ;
   10.60      orders: ( 'max' | 'min' | 'ms' ) *
   10.61 -  "}
   10.62 +  \<close>}
   10.63  
   10.64    \begin{description}
   10.65  
   10.66 @@ -574,11 +574,11 @@
   10.67      @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
   10.68    \end{matharray}
   10.69  
   10.70 -  @{rail "
   10.71 +  @{rail \<open>
   10.72      @@{command (HOL) partial_function} @{syntax target}?
   10.73 -      '(' @{syntax nameref} ')' @{syntax \"fixes\"} \<newline>
   10.74 +      '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
   10.75        @'where' @{syntax thmdecl}? @{syntax prop}
   10.76 -  "}
   10.77 +  \<close>}
   10.78  
   10.79    \begin{description}
   10.80  
   10.81 @@ -649,7 +649,7 @@
   10.82    "recdef_tc"} for defining recursive are mostly obsolete; @{command
   10.83    (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
   10.84  
   10.85 -  @{rail "
   10.86 +  @{rail \<open>
   10.87      @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
   10.88        @{syntax name} @{syntax term} (@{syntax prop} +) hints?
   10.89      ;
   10.90 @@ -661,7 +661,7 @@
   10.91        (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
   10.92      ;
   10.93      tc: @{syntax nameref} ('(' @{syntax nat} ')')?
   10.94 -  "}
   10.95 +  \<close>}
   10.96  
   10.97    \begin{description}
   10.98  
   10.99 @@ -695,10 +695,10 @@
  10.100      @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
  10.101    \end{matharray}
  10.102  
  10.103 -  @{rail "
  10.104 +  @{rail \<open>
  10.105      (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
  10.106        @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
  10.107 -  "}
  10.108 +  \<close>}
  10.109  *}
  10.110  
  10.111  
  10.112 @@ -710,7 +710,7 @@
  10.113      @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
  10.114    \end{matharray}
  10.115  
  10.116 -  @{rail "
  10.117 +  @{rail \<open>
  10.118      @@{command (HOL) datatype} (spec + @'and')
  10.119      ;
  10.120      @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
  10.121 @@ -719,7 +719,7 @@
  10.122      spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
  10.123      ;
  10.124      cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
  10.125 -  "}
  10.126 +  \<close>}
  10.127  
  10.128    \begin{description}
  10.129  
  10.130 @@ -873,12 +873,12 @@
  10.131      @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
  10.132    \end{matharray}
  10.133  
  10.134 -  @{rail "
  10.135 +  @{rail \<open>
  10.136      @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
  10.137        (@{syntax type} '+')? (constdecl +)
  10.138      ;
  10.139      constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
  10.140 -  "}
  10.141 +  \<close>}
  10.142  
  10.143    \begin{description}
  10.144  
  10.145 @@ -1074,14 +1074,13 @@
  10.146    type_synonym} from Isabelle/Pure merely introduces syntactic
  10.147    abbreviations, without any logical significance.
  10.148  
  10.149 -  @{rail "
  10.150 +  @{rail \<open>
  10.151      @@{command (HOL) typedef} abs_type '=' rep_set
  10.152      ;
  10.153 -
  10.154      abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
  10.155      ;
  10.156      rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
  10.157 -  "}
  10.158 +  \<close>}
  10.159  
  10.160    \begin{description}
  10.161  
  10.162 @@ -1198,10 +1197,9 @@
  10.163      @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  10.164    \end{matharray}
  10.165  
  10.166 -  @{rail "
  10.167 +  @{rail \<open>
  10.168      @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
  10.169 -    ;
  10.170 -  "}
  10.171 +  \<close>}
  10.172  
  10.173    \begin{description}
  10.174  
  10.175 @@ -1265,28 +1263,26 @@
  10.176    packages. The user should consider using these two new packages for
  10.177    lifting definitions and transporting theorems.
  10.178  
  10.179 -  @{rail "
  10.180 -    @@{command (HOL) quotient_type} (spec);
  10.181 -
  10.182 +  @{rail \<open>
  10.183 +    @@{command (HOL) quotient_type} (spec)
  10.184 +    ;
  10.185      spec: @{syntax typespec} @{syntax mixfix}? '=' \<newline>
  10.186       @{syntax type} '/' ('partial' ':')? @{syntax term} \<newline>
  10.187 -     (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?;
  10.188 -  "}
  10.189 -
  10.190 -  @{rail "
  10.191 +     (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?
  10.192 +  \<close>}
  10.193 +
  10.194 +  @{rail \<open>
  10.195      @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
  10.196 -    @{syntax term} 'is' @{syntax term};
  10.197 -
  10.198 +    @{syntax term} 'is' @{syntax term}
  10.199 +    ;
  10.200      constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
  10.201 -  "}
  10.202 -
  10.203 -  @{rail "
  10.204 +  \<close>}
  10.205 +
  10.206 +  @{rail \<open>
  10.207      @@{method (HOL) lifting} @{syntax thmrefs}?
  10.208      ;
  10.209 -
  10.210      @@{method (HOL) lifting_setup} @{syntax thmrefs}?
  10.211 -    ;
  10.212 -  "}
  10.213 +  \<close>}
  10.214  
  10.215    \begin{description}
  10.216  
  10.217 @@ -1399,12 +1395,12 @@
  10.218      @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
  10.219    \end{matharray}
  10.220  
  10.221 -  @{rail "
  10.222 -  (@@{command (HOL) specification} | @@{command (HOL) ax_specification})
  10.223 -    '(' (decl +) ')' \<newline> (@{syntax thmdecl}? @{syntax prop} +)
  10.224 -  ;
  10.225 -  decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
  10.226 -  "}
  10.227 +  @{rail \<open>
  10.228 +    (@@{command (HOL) specification} | @@{command (HOL) ax_specification})
  10.229 +      '(' (decl +) ')' \<newline> (@{syntax thmdecl}? @{syntax prop} +)
  10.230 +    ;
  10.231 +    decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
  10.232 +  \<close>}
  10.233  
  10.234    \begin{description}
  10.235  
  10.236 @@ -1458,10 +1454,10 @@
  10.237    @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
  10.238    @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
  10.239  
  10.240 -  @{rail "
  10.241 +  @{rail \<open>
  10.242      (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
  10.243 -    (@{syntax nameref} (@{syntax term} + ) + @'and')
  10.244 -  "}
  10.245 +      (@{syntax nameref} (@{syntax term} + ) + @'and')
  10.246 +  \<close>}
  10.247  
  10.248    \begin{description}
  10.249  
  10.250 @@ -1490,9 +1486,9 @@
  10.251      @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
  10.252    \end{matharray}
  10.253  
  10.254 -  @{rail "
  10.255 +  @{rail \<open>
  10.256      @@{attribute (HOL) split_format} ('(' 'complete' ')')?
  10.257 -  "}
  10.258 +  \<close>}
  10.259  
  10.260    \begin{description}
  10.261  
  10.262 @@ -1626,27 +1622,27 @@
  10.263      @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\   
  10.264    \end{matharray}
  10.265  
  10.266 -  @{rail "
  10.267 +  @{rail \<open>
  10.268      @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \<newline>
  10.269        @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
  10.270 -  "}
  10.271 -
  10.272 -  @{rail "
  10.273 +  \<close>}
  10.274 +
  10.275 +  @{rail \<open>
  10.276      @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>
  10.277        'is' @{syntax term} (@'parametric' @{syntax thmref})?;
  10.278 -  "}
  10.279 -
  10.280 -  @{rail "
  10.281 +  \<close>}
  10.282 +
  10.283 +  @{rail \<open>
  10.284      @@{command (HOL) lifting_forget} @{syntax nameref};
  10.285 -  "}
  10.286 -
  10.287 -  @{rail "
  10.288 +  \<close>}
  10.289 +
  10.290 +  @{rail \<open>
  10.291      @@{command (HOL) lifting_update} @{syntax nameref};
  10.292 -  "}
  10.293 -
  10.294 -  @{rail "
  10.295 +  \<close>}
  10.296 +
  10.297 +  @{rail \<open>
  10.298      @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
  10.299 -  "}
  10.300 +  \<close>}
  10.301  
  10.302    \begin{description}
  10.303  
  10.304 @@ -1828,14 +1824,11 @@
  10.305    them as necessary when parsing a term. See
  10.306    \cite{traytel-berghofer-nipkow-2011} for details.
  10.307  
  10.308 -  @{rail "
  10.309 +  @{rail \<open>
  10.310      @@{attribute (HOL) coercion} (@{syntax term})?
  10.311      ;
  10.312 -  "}
  10.313 -  @{rail "
  10.314      @@{attribute (HOL) coercion_map} (@{syntax term})?
  10.315 -    ;
  10.316 -  "}
  10.317 +  \<close>}
  10.318  
  10.319    \begin{description}
  10.320  
  10.321 @@ -1902,9 +1895,9 @@
  10.322      @{method_def (HOL) iprover} & : & @{text method} \\
  10.323    \end{matharray}
  10.324  
  10.325 -  @{rail "
  10.326 -    @@{method (HOL) iprover} ( @{syntax rulemod} * )
  10.327 -  "}
  10.328 +  @{rail \<open>
  10.329 +    @@{method (HOL) iprover} (@{syntax rulemod} *)
  10.330 +  \<close>}
  10.331  
  10.332    \begin{description}
  10.333  
  10.334 @@ -1934,14 +1927,13 @@
  10.335      @{method_def (HOL) "metis"} & : & @{text method} \\
  10.336    \end{matharray}
  10.337  
  10.338 -  @{rail "
  10.339 +  @{rail \<open>
  10.340      @@{method (HOL) meson} @{syntax thmrefs}?
  10.341      ;
  10.342 -
  10.343      @@{method (HOL) metis}
  10.344        ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
  10.345        @{syntax thmrefs}?
  10.346 -  "}
  10.347 +  \<close>}
  10.348  
  10.349    \begin{description}
  10.350  
  10.351 @@ -1968,13 +1960,13 @@
  10.352      @{attribute_def (HOL) algebra} & : & @{text attribute} \\
  10.353    \end{matharray}
  10.354  
  10.355 -  @{rail "
  10.356 +  @{rail \<open>
  10.357      @@{method (HOL) algebra}
  10.358        ('add' ':' @{syntax thmrefs})?
  10.359        ('del' ':' @{syntax thmrefs})?
  10.360      ;
  10.361      @@{attribute (HOL) algebra} (() | 'add' | 'del')
  10.362 -  "}
  10.363 +  \<close>}
  10.364  
  10.365    \begin{description}
  10.366  
  10.367 @@ -2051,9 +2043,9 @@
  10.368      @{method_def (HOL) "coherent"} & : & @{text method} \\
  10.369    \end{matharray}
  10.370  
  10.371 -  @{rail "
  10.372 +  @{rail \<open>
  10.373      @@{method (HOL) coherent} @{syntax thmrefs}?
  10.374 -  "}
  10.375 +  \<close>}
  10.376  
  10.377    \begin{description}
  10.378  
  10.379 @@ -2081,7 +2073,7 @@
  10.380      @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
  10.381    \end{matharray}
  10.382  
  10.383 -  @{rail "
  10.384 +  @{rail \<open>
  10.385      @@{command (HOL) try}
  10.386      ;
  10.387  
  10.388 @@ -2094,13 +2086,10 @@
  10.389  
  10.390      @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
  10.391      ;
  10.392 -
  10.393      args: ( @{syntax name} '=' value + ',' )
  10.394      ;
  10.395 -
  10.396      facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
  10.397 -    ;
  10.398 -  "} % FIXME check args "value"
  10.399 +  \<close>} % FIXME check args "value"
  10.400  
  10.401    \begin{description}
  10.402  
  10.403 @@ -2150,7 +2139,7 @@
  10.404      @{command_def (HOL) "find_unused_assms"} & : & @{text "context \<rightarrow>"}
  10.405    \end{matharray}
  10.406  
  10.407 -  @{rail "
  10.408 +  @{rail \<open>
  10.409      @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
  10.410      ;
  10.411  
  10.412 @@ -2171,13 +2160,10 @@
  10.413  
  10.414      @@{command (HOL) find_unused_assms} @{syntax name}?
  10.415      ;
  10.416 -
  10.417      modes: '(' (@{syntax name} +) ')'
  10.418      ;
  10.419 -
  10.420      args: ( @{syntax name} '=' value + ',' )
  10.421 -    ;
  10.422 -  "} % FIXME check "value"
  10.423 +  \<close>} % FIXME check "value"
  10.424  
  10.425    \begin{description}
  10.426  
  10.427 @@ -2320,7 +2306,7 @@
  10.428      @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
  10.429    \end{matharray}
  10.430  
  10.431 -  @{rail "
  10.432 +  @{rail \<open>
  10.433      @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
  10.434      ;
  10.435      @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
  10.436 @@ -2329,9 +2315,8 @@
  10.437      ;
  10.438      @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
  10.439      ;
  10.440 -
  10.441      rule: 'rule' ':' @{syntax thmref}
  10.442 -  "}
  10.443 +  \<close>}
  10.444  
  10.445    \begin{description}
  10.446  
  10.447 @@ -2413,7 +2398,7 @@
  10.448      @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
  10.449    \end{matharray}
  10.450  
  10.451 -  @{rail "
  10.452 +  @{rail \<open>
  10.453      @@{command (HOL) export_code} ( constexpr + ) \<newline>
  10.454         ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
  10.455          ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
  10.456 @@ -2553,7 +2538,7 @@
  10.457      ;
  10.458  
  10.459      modes: mode @'as' const
  10.460 -  "}
  10.461 +  \<close>}
  10.462  
  10.463    \begin{description}
  10.464  
    11.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Wed Jan 22 10:13:40 2014 +0100
    11.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Wed Jan 22 17:14:27 2014 +0100
    11.3 @@ -46,7 +46,7 @@
    11.4    These diagnostic commands assist interactive development by printing
    11.5    internal logical entities in a human-readable fashion.
    11.6  
    11.7 -  @{rail "
    11.8 +  @{rail \<open>
    11.9      @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
   11.10      ;
   11.11      @@{command term} @{syntax modes}? @{syntax term}
   11.12 @@ -59,9 +59,8 @@
   11.13      ;
   11.14      @@{command print_state} @{syntax modes}?
   11.15      ;
   11.16 -
   11.17      @{syntax_def modes}: '(' (@{syntax name} + ) ')'
   11.18 -  "}
   11.19 +  \<close>}
   11.20  
   11.21    \begin{description}
   11.22  
   11.23 @@ -358,7 +357,7 @@
   11.24    to specify any context-free priority grammar, which is more general
   11.25    than the fixity declarations of ML and Prolog.
   11.26  
   11.27 -  @{rail "
   11.28 +  @{rail \<open>
   11.29      @{syntax_def mixfix}: '('
   11.30        @{syntax template} prios? @{syntax nat}? |
   11.31        (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
   11.32 @@ -369,7 +368,7 @@
   11.33      template: string
   11.34      ;
   11.35      prios: '[' (@{syntax nat} + ',') ']'
   11.36 -  "}
   11.37 +  \<close>}
   11.38  
   11.39    The string given as @{text template} may include literal text,
   11.40    spacing, blocks, and arguments (denoted by ``@{text _}''); the
   11.41 @@ -559,7 +558,7 @@
   11.42    allows to add or delete mixfix annotations for of existing logical
   11.43    entities within the current context.
   11.44  
   11.45 -  @{rail "
   11.46 +  @{rail \<open>
   11.47      (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
   11.48        @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
   11.49      ;
   11.50 @@ -567,7 +566,7 @@
   11.51        (@{syntax nameref} @{syntax mixfix} + @'and')
   11.52      ;
   11.53      @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
   11.54 -  "}
   11.55 +  \<close>}
   11.56  
   11.57    \begin{description}
   11.58  
   11.59 @@ -631,18 +630,19 @@
   11.60      @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
   11.61      @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
   11.62      @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
   11.63 -
   11.64      @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
   11.65 +    @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
   11.66      @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
   11.67    \end{supertabular}
   11.68    \end{center}
   11.69  
   11.70    The token categories @{syntax (inner) num_token}, @{syntax (inner)
   11.71    float_token}, @{syntax (inner) xnum_token}, @{syntax (inner)
   11.72 -  str_token}, and @{syntax (inner) cartouche} are not used in Pure.
   11.73 -  Object-logics may implement numerals and string literals by adding
   11.74 -  appropriate syntax declarations, together with some translation
   11.75 -  functions (e.g.\ see Isabelle/HOL).
   11.76 +  str_token}, @{syntax (inner) string_token}, and @{syntax (inner)
   11.77 +  cartouche} are not used in Pure. Object-logics may implement
   11.78 +  numerals and string literals by adding appropriate syntax
   11.79 +  declarations, together with some translation functions (e.g.\ see
   11.80 +  @{file "~~/src/HOL/Tools/string_syntax.ML"}).
   11.81  
   11.82    The derived categories @{syntax_def (inner) num_const}, @{syntax_def
   11.83    (inner) float_const}, and @{syntax_def (inner) num_const} provide
   11.84 @@ -1216,7 +1216,7 @@
   11.85    @{command translations}) are required to turn resulting parse trees
   11.86    into proper representations of formal entities again.
   11.87  
   11.88 -  @{rail "
   11.89 +  @{rail \<open>
   11.90      @@{command nonterminal} (@{syntax name} + @'and')
   11.91      ;
   11.92      (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
   11.93 @@ -1230,7 +1230,7 @@
   11.94      mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
   11.95      ;
   11.96      transpat: ('(' @{syntax nameref} ')')? @{syntax string}
   11.97 -  "}
   11.98 +  \<close>}
   11.99  
  11.100    \begin{description}
  11.101  
  11.102 @@ -1463,7 +1463,7 @@
  11.103    manipulations of inner syntax, at the expense of some complexity and
  11.104    obscurity in the implementation.
  11.105  
  11.106 -  @{rail "
  11.107 +  @{rail \<open>
  11.108    ( @@{command parse_ast_translation} | @@{command parse_translation} |
  11.109      @@{command print_translation} | @@{command typed_print_translation} |
  11.110      @@{command print_ast_translation}) @{syntax text}
  11.111 @@ -1472,7 +1472,7 @@
  11.112     @@{ML_antiquotation type_syntax} |
  11.113     @@{ML_antiquotation const_syntax} |
  11.114     @@{ML_antiquotation syntax_const}) name
  11.115 -  "}
  11.116 +  \<close>}
  11.117  
  11.118    \begin{description}
  11.119  
    12.1 --- a/src/Doc/IsarRef/Misc.thy	Wed Jan 22 10:13:40 2014 +0100
    12.2 +++ b/src/Doc/IsarRef/Misc.thy	Wed Jan 22 17:14:27 2014 +0100
    12.3 @@ -20,7 +20,7 @@
    12.4      @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    12.5    \end{matharray}
    12.6  
    12.7 -  @{rail "
    12.8 +  @{rail \<open>
    12.9      (@@{command print_theory} | @@{command print_theorems}) ('!'?)
   12.10      ;
   12.11  
   12.12 @@ -37,7 +37,7 @@
   12.13      @@{command thm_deps} @{syntax thmrefs}
   12.14      ;
   12.15      @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
   12.16 -  "}
   12.17 +  \<close>}
   12.18  
   12.19    These commands print certain parts of the theory and proof context.
   12.20    Note that there are some further ones available, such as for the set
   12.21 @@ -121,9 +121,9 @@
   12.22      @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   12.23    \end{matharray}
   12.24  
   12.25 -  @{rail "
   12.26 +  @{rail \<open>
   12.27      (@@{command cd} | @@{command use_thy}) @{syntax name}
   12.28 -  "}
   12.29 +  \<close>}
   12.30  
   12.31    \begin{description}
   12.32  
    13.1 --- a/src/Doc/IsarRef/Outer_Syntax.thy	Wed Jan 22 10:13:40 2014 +0100
    13.2 +++ b/src/Doc/IsarRef/Outer_Syntax.thy	Wed Jan 22 17:14:27 2014 +0100
    13.3 @@ -72,9 +72,9 @@
    13.4      @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    13.5    \end{matharray}
    13.6  
    13.7 -  @{rail "
    13.8 +  @{rail \<open>
    13.9      @@{command help} (@{syntax name} * )
   13.10 -  "}
   13.11 +  \<close>}
   13.12  
   13.13    \begin{description}
   13.14  
   13.15 @@ -233,14 +233,14 @@
   13.16    Already existing objects are usually referenced by @{syntax
   13.17    nameref}.
   13.18  
   13.19 -  @{rail "
   13.20 +  @{rail \<open>
   13.21      @{syntax_def name}: @{syntax ident} | @{syntax symident} |
   13.22        @{syntax string} | @{syntax nat}
   13.23      ;
   13.24      @{syntax_def parname}: '(' @{syntax name} ')'
   13.25      ;
   13.26      @{syntax_def nameref}: @{syntax name} | @{syntax longident}
   13.27 -  "}
   13.28 +  \<close>}
   13.29  *}
   13.30  
   13.31  
   13.32 @@ -250,11 +250,11 @@
   13.33    natural numbers and floating point numbers.  These are combined as
   13.34    @{syntax int} and @{syntax real} as follows.
   13.35  
   13.36 -  @{rail "
   13.37 +  @{rail \<open>
   13.38      @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
   13.39      ;
   13.40      @{syntax_def real}: @{syntax float} | @{syntax int}
   13.41 -  "}
   13.42 +  \<close>}
   13.43  
   13.44    Note that there is an overlap with the category @{syntax name},
   13.45    which also includes @{syntax nat}.
   13.46 @@ -271,11 +271,11 @@
   13.47    @{verbatim "--"}~@{syntax text}.  Any number of these may occur
   13.48    within Isabelle/Isar commands.
   13.49  
   13.50 -  @{rail "
   13.51 +  @{rail \<open>
   13.52      @{syntax_def text}: @{syntax verbatim} | @{syntax nameref}
   13.53      ;
   13.54      @{syntax_def comment}: '--' @{syntax text}
   13.55 -  "}
   13.56 +  \<close>}
   13.57  *}
   13.58  
   13.59  
   13.60 @@ -288,13 +288,13 @@
   13.61    intersection of these classes.  The syntax of type arities is given
   13.62    directly at the outer level.
   13.63  
   13.64 -  @{rail "
   13.65 +  @{rail \<open>
   13.66      @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
   13.67      ;
   13.68      @{syntax_def sort}: @{syntax nameref}
   13.69      ;
   13.70      @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
   13.71 -  "}
   13.72 +  \<close>}
   13.73  *}
   13.74  
   13.75  
   13.76 @@ -314,38 +314,38 @@
   13.77    by commands or other keywords already (such as @{verbatim "="} or
   13.78    @{verbatim "+"}).
   13.79  
   13.80 -  @{rail "
   13.81 +  @{rail \<open>
   13.82      @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
   13.83        @{syntax typevar}
   13.84      ;
   13.85      @{syntax_def term}: @{syntax nameref} | @{syntax var}
   13.86      ;
   13.87      @{syntax_def prop}: @{syntax term}
   13.88 -  "}
   13.89 +  \<close>}
   13.90  
   13.91    Positional instantiations are indicated by giving a sequence of
   13.92    terms, or the placeholder ``@{text _}'' (underscore), which means to
   13.93    skip a position.
   13.94  
   13.95 -  @{rail "
   13.96 +  @{rail \<open>
   13.97      @{syntax_def inst}: '_' | @{syntax term}
   13.98      ;
   13.99      @{syntax_def insts}: (@{syntax inst} *)
  13.100 -  "}
  13.101 +  \<close>}
  13.102  
  13.103    Type declarations and definitions usually refer to @{syntax
  13.104    typespec} on the left-hand side.  This models basic type constructor
  13.105    application at the outer syntax level.  Note that only plain postfix
  13.106    notation is available here, but no infixes.
  13.107  
  13.108 -  @{rail "
  13.109 +  @{rail \<open>
  13.110      @{syntax_def typespec}:
  13.111        (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
  13.112      ;
  13.113      @{syntax_def typespec_sorts}:
  13.114        (() | (@{syntax typefree} ('::' @{syntax sort})?) |
  13.115          '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
  13.116 -  "}
  13.117 +  \<close>}
  13.118  *}
  13.119  
  13.120  
  13.121 @@ -356,11 +356,11 @@
  13.122    specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}''.
  13.123    This works both for @{syntax term} and @{syntax prop}.
  13.124  
  13.125 -  @{rail "
  13.126 +  @{rail \<open>
  13.127      @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
  13.128      ;
  13.129      @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
  13.130 -  "}
  13.131 +  \<close>}
  13.132  
  13.133    \medskip Declarations of local variables @{text "x :: \<tau>"} and
  13.134    logical propositions @{text "a : \<phi>"} represent different views on
  13.135 @@ -370,11 +370,11 @@
  13.136    references of current facts).  In any case, Isar proof elements
  13.137    usually admit to introduce multiple such items simultaneously.
  13.138  
  13.139 -  @{rail "
  13.140 +  @{rail \<open>
  13.141      @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
  13.142      ;
  13.143      @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
  13.144 -  "}
  13.145 +  \<close>}
  13.146  
  13.147    The treatment of multiple declarations corresponds to the
  13.148    complementary focus of @{syntax vars} versus @{syntax props}.  In
  13.149 @@ -398,7 +398,7 @@
  13.150    any atomic entity, including any @{syntax keyword} conforming to
  13.151    @{syntax symident}.
  13.152  
  13.153 -  @{rail "
  13.154 +  @{rail \<open>
  13.155      @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
  13.156        @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
  13.157        @{syntax keyword} | @{syntax cartouche}
  13.158 @@ -408,7 +408,7 @@
  13.159      @{syntax_def args}: arg *
  13.160      ;
  13.161      @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
  13.162 -  "}
  13.163 +  \<close>}
  13.164  
  13.165    Theorem specifications come in several flavors: @{syntax axmdecl}
  13.166    and @{syntax thmdecl} usually refer to axioms, assumptions or
  13.167 @@ -443,7 +443,7 @@
  13.168    This form of in-place declarations is particularly useful with
  13.169    commands like @{command "declare"} and @{command "using"}.
  13.170  
  13.171 -  @{rail "
  13.172 +  @{rail \<open>
  13.173      @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
  13.174      ;
  13.175      @{syntax_def thmdecl}: thmbind ':'
  13.176 @@ -460,7 +460,7 @@
  13.177      thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
  13.178      ;
  13.179      selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
  13.180 -  "}
  13.181 +  \<close>}
  13.182  *}
  13.183  
  13.184  end
    14.1 --- a/src/Doc/IsarRef/Proof.thy	Wed Jan 22 10:13:40 2014 +0100
    14.2 +++ b/src/Doc/IsarRef/Proof.thy	Wed Jan 22 17:14:27 2014 +0100
    14.3 @@ -53,11 +53,11 @@
    14.4      @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
    14.5    \end{matharray}
    14.6  
    14.7 -  @{rail "
    14.8 +  @{rail \<open>
    14.9      @@{command notepad} @'begin'
   14.10      ;
   14.11      @@{command end}
   14.12 -  "}
   14.13 +  \<close>}
   14.14  
   14.15    \begin{description}
   14.16  
   14.17 @@ -183,7 +183,7 @@
   14.18    exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
   14.19    \<phi>[t]"}.
   14.20  
   14.21 -  @{rail "
   14.22 +  @{rail \<open>
   14.23      @@{command fix} (@{syntax vars} + @'and')
   14.24      ;
   14.25      (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
   14.26 @@ -192,7 +192,7 @@
   14.27      ;
   14.28      def: @{syntax thmdecl}? \<newline>
   14.29        @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
   14.30 -  "}
   14.31 +  \<close>}
   14.32  
   14.33    \begin{description}
   14.34    
   14.35 @@ -262,9 +262,9 @@
   14.36    input process just after type checking.  Also note that @{command
   14.37    "def"} does not support polymorphism.
   14.38  
   14.39 -  @{rail "
   14.40 +  @{rail \<open>
   14.41      @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
   14.42 -  "}
   14.43 +  \<close>}
   14.44  
   14.45    The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
   14.46    @{syntax prop_pat} (see \secref{sec:term-decls}).
   14.47 @@ -318,12 +318,12 @@
   14.48    to the most recently established facts, but only \emph{before}
   14.49    issuing a follow-up claim.
   14.50  
   14.51 -  @{rail "
   14.52 +  @{rail \<open>
   14.53      @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   14.54      ;
   14.55      (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
   14.56        (@{syntax thmrefs} + @'and')
   14.57 -  "}
   14.58 +  \<close>}
   14.59  
   14.60    \begin{description}
   14.61  
   14.62 @@ -429,7 +429,7 @@
   14.63    contexts of (essentially a big disjunction of eliminated parameters
   14.64    and assumptions, cf.\ \secref{sec:obtain}).
   14.65  
   14.66 -  @{rail "
   14.67 +  @{rail \<open>
   14.68      (@@{command lemma} | @@{command theorem} | @@{command corollary} |
   14.69       @@{command schematic_lemma} | @@{command schematic_theorem} |
   14.70       @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)
   14.71 @@ -441,12 +441,12 @@
   14.72    
   14.73      goal: (@{syntax props} + @'and')
   14.74      ;
   14.75 -    longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion
   14.76 +    longgoal: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} * ) conclusion
   14.77      ;
   14.78      conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
   14.79      ;
   14.80      case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
   14.81 -  "}
   14.82 +  \<close>}
   14.83  
   14.84    \begin{description}
   14.85    
   14.86 @@ -541,12 +541,12 @@
   14.87    nameref}~@{syntax args} specifications.  Note that parentheses may
   14.88    be dropped for single method specifications (with no arguments).
   14.89  
   14.90 -  @{rail "
   14.91 +  @{rail \<open>
   14.92      @{syntax_def method}:
   14.93        (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
   14.94      ;
   14.95      methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|')
   14.96 -  "}
   14.97 +  \<close>}
   14.98  
   14.99    Proper Isar proof methods do \emph{not} admit arbitrary goal
  14.100    addressing, but refer either to the first sub-goal or all sub-goals
  14.101 @@ -564,10 +564,10 @@
  14.102    all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
  14.103    "n"}.
  14.104  
  14.105 -  @{rail "
  14.106 +  @{rail \<open>
  14.107      @{syntax_def goal_spec}:
  14.108        '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
  14.109 -  "}
  14.110 +  \<close>}
  14.111  *}
  14.112  
  14.113  
  14.114 @@ -621,15 +621,15 @@
  14.115    default terminal method.  Any remaining goals are always solved by
  14.116    assumption in the very last step.
  14.117  
  14.118 -  @{rail "
  14.119 +  @{rail \<open>
  14.120      @@{command proof} method?
  14.121      ;
  14.122      @@{command qed} method?
  14.123      ;
  14.124 -    @@{command \"by\"} method method?
  14.125 +    @@{command "by"} method method?
  14.126      ;
  14.127 -    (@@{command \".\"} | @@{command \"..\"} | @@{command sorry})
  14.128 -  "}
  14.129 +    (@@{command "."} | @@{command ".."} | @@{command sorry})
  14.130 +  \<close>}
  14.131  
  14.132    \begin{description}
  14.133    
  14.134 @@ -706,7 +706,7 @@
  14.135      @{attribute_def "where"} & : & @{text attribute} \\
  14.136    \end{matharray}
  14.137  
  14.138 -  @{rail "
  14.139 +  @{rail \<open>
  14.140      @@{method fact} @{syntax thmrefs}?
  14.141      ;
  14.142      @@{method (Pure) rule} @{syntax thmrefs}?
  14.143 @@ -723,10 +723,10 @@
  14.144      ;
  14.145      @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
  14.146      ;
  14.147 -    @@{attribute \"where\"}
  14.148 +    @@{attribute "where"}
  14.149        ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
  14.150        (@{syntax type} | @{syntax term}) * @'and')
  14.151 -  "}
  14.152 +  \<close>}
  14.153  
  14.154    \begin{description}
  14.155    
  14.156 @@ -846,13 +846,13 @@
  14.157      @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
  14.158    \end{matharray}
  14.159  
  14.160 -  @{rail "
  14.161 +  @{rail \<open>
  14.162      ( @@{command apply} | @@{command apply_end} ) @{syntax method}
  14.163      ;
  14.164      @@{command defer} @{syntax nat}?
  14.165      ;
  14.166      @@{command prefer} @{syntax nat}
  14.167 -  "}
  14.168 +  \<close>}
  14.169  
  14.170    \begin{description}
  14.171  
  14.172 @@ -907,10 +907,9 @@
  14.173      @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
  14.174    \end{matharray}
  14.175  
  14.176 -  @{rail "
  14.177 +  @{rail \<open>
  14.178      @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
  14.179 -    ;
  14.180 -  "}
  14.181 +  \<close>}
  14.182  
  14.183    \begin{description}
  14.184  
  14.185 @@ -963,12 +962,12 @@
  14.186    later, provided that the corresponding parameters do \emph{not}
  14.187    occur in the conclusion.
  14.188  
  14.189 -  @{rail "
  14.190 +  @{rail \<open>
  14.191      @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')
  14.192        @'where' (@{syntax props} + @'and')
  14.193      ;
  14.194      @@{command guess} (@{syntax vars} + @'and')
  14.195 -  "}
  14.196 +  \<close>}
  14.197  
  14.198    The derived Isar command @{command "obtain"} is defined as follows
  14.199    (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
  14.200 @@ -1078,11 +1077,11 @@
  14.201      @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
  14.202    \end{matharray}
  14.203  
  14.204 -  @{rail "
  14.205 +  @{rail \<open>
  14.206      (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?
  14.207      ;
  14.208      @@{attribute trans} (() | 'add' | 'del')
  14.209 -  "}
  14.210 +  \<close>}
  14.211  
  14.212    \begin{description}
  14.213  
  14.214 @@ -1195,7 +1194,7 @@
  14.215    derived manually become ready to use in advanced case analysis
  14.216    later.
  14.217  
  14.218 -  @{rail "
  14.219 +  @{rail \<open>
  14.220      @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
  14.221      ;
  14.222      caseref: nameref attributes?
  14.223 @@ -1208,7 +1207,7 @@
  14.224      @@{attribute params} ((@{syntax name} * ) + @'and')
  14.225      ;
  14.226      @@{attribute consumes} @{syntax int}?
  14.227 -  "}
  14.228 +  \<close>}
  14.229  
  14.230    \begin{description}
  14.231    
  14.232 @@ -1303,7 +1302,7 @@
  14.233    the names of the facts in the local context invoked by the @{command "case"}
  14.234    command.
  14.235  
  14.236 -  @{rail "
  14.237 +  @{rail \<open>
  14.238      @@{method cases} ('(' 'no_simp' ')')? \<newline>
  14.239        (@{syntax insts} * @'and') rule?
  14.240      ;
  14.241 @@ -1322,7 +1321,7 @@
  14.242      arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
  14.243      ;
  14.244      taking: 'taking' ':' @{syntax insts}
  14.245 -  "}
  14.246 +  \<close>}
  14.247  
  14.248    \begin{description}
  14.249  
  14.250 @@ -1499,7 +1498,7 @@
  14.251      @{attribute_def coinduct} & : & @{text attribute} \\
  14.252    \end{matharray}
  14.253  
  14.254 -  @{rail "
  14.255 +  @{rail \<open>
  14.256      @@{attribute cases} spec
  14.257      ;
  14.258      @@{attribute induct} spec
  14.259 @@ -1508,7 +1507,7 @@
  14.260      ;
  14.261  
  14.262      spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
  14.263 -  "}
  14.264 +  \<close>}
  14.265  
  14.266    \begin{description}
  14.267  
    15.1 --- a/src/Doc/IsarRef/Spec.thy	Wed Jan 22 10:13:40 2014 +0100
    15.2 +++ b/src/Doc/IsarRef/Spec.thy	Wed Jan 22 17:14:27 2014 +0100
    15.3 @@ -50,7 +50,7 @@
    15.4    although some user-interfaces might pretend that trailing input is
    15.5    admissible.
    15.6  
    15.7 -  @{rail "
    15.8 +  @{rail \<open>
    15.9      @@{command theory} @{syntax name} imports keywords? \<newline> @'begin'
   15.10      ;
   15.11      imports: @'imports' (@{syntax name} +)
   15.12 @@ -59,7 +59,7 @@
   15.13      ;
   15.14      keyword_decls: (@{syntax string} +)
   15.15        ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
   15.16 -  "}
   15.17 +  \<close>}
   15.18  
   15.19    \begin{description}
   15.20  
   15.21 @@ -121,13 +121,13 @@
   15.22    targets, like @{command "locale"}, @{command "class"}, @{command
   15.23    "instantiation"}, @{command "overloading"}.
   15.24  
   15.25 -  @{rail "
   15.26 +  @{rail \<open>
   15.27      @@{command context} @{syntax nameref} @'begin'
   15.28      ;
   15.29 -    @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin'
   15.30 +    @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
   15.31      ;
   15.32      @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
   15.33 -  "}
   15.34 +  \<close>}
   15.35  
   15.36    \begin{description}
   15.37    
   15.38 @@ -210,14 +210,14 @@
   15.39    without logical dependencies, which is in contrast to locales and
   15.40    locale interpretation (\secref{sec:locale}).
   15.41  
   15.42 -  @{rail "
   15.43 +  @{rail \<open>
   15.44      @@{command bundle} @{syntax target}? \<newline>
   15.45      @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
   15.46      ;
   15.47      (@@{command include} | @@{command including}) (@{syntax nameref}+)
   15.48      ;
   15.49 -    @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+)
   15.50 -  "}
   15.51 +    @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
   15.52 +  \<close>}
   15.53  
   15.54    \begin{description}
   15.55  
   15.56 @@ -274,8 +274,8 @@
   15.57    "defs"} (see \secref{sec:consts}), and raw axioms.  In particular,
   15.58    type-inference covers the whole specification as usual.
   15.59  
   15.60 -  @{rail "
   15.61 -    @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
   15.62 +  @{rail \<open>
   15.63 +    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
   15.64      ;
   15.65      @@{command definition} @{syntax target}? \<newline>
   15.66        (decl @'where')? @{syntax thmdecl}? @{syntax prop}
   15.67 @@ -284,13 +284,13 @@
   15.68        (decl @'where')? @{syntax prop}
   15.69      ;
   15.70  
   15.71 -    @{syntax_def \"fixes\"}: ((@{syntax name} ('::' @{syntax type})?
   15.72 +    @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
   15.73        @{syntax mixfix}? | @{syntax vars}) + @'and')
   15.74      ;
   15.75      specs: (@{syntax thmdecl}? @{syntax props} + @'and')
   15.76      ;
   15.77      decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
   15.78 -  "}
   15.79 +  \<close>}
   15.80  
   15.81    \begin{description}
   15.82    
   15.83 @@ -364,12 +364,12 @@
   15.84    case: it consists of a theorem which is applied to the context by
   15.85    means of an attribute.
   15.86  
   15.87 -  @{rail "
   15.88 +  @{rail \<open>
   15.89      (@@{command declaration} | @@{command syntax_declaration})
   15.90        ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
   15.91      ;
   15.92      @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
   15.93 -  "}
   15.94 +  \<close>}
   15.95  
   15.96    \begin{description}
   15.97  
   15.98 @@ -431,8 +431,8 @@
   15.99    elements from the locale instances.  Redundant locale instances are
  15.100    omitted according to roundup.
  15.101  
  15.102 -  @{rail "
  15.103 -    @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
  15.104 +  @{rail \<open>
  15.105 +    @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax "fixes"} + @'and'))?
  15.106      ;
  15.107      instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
  15.108      ;
  15.109 @@ -441,7 +441,7 @@
  15.110      pos_insts: ('_' | @{syntax term})*
  15.111      ;
  15.112      named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
  15.113 -  "}
  15.114 +  \<close>}
  15.115  
  15.116    A locale instance consists of a reference to a locale and either
  15.117    positional or named parameter instantiations.  Identical
  15.118 @@ -483,7 +483,7 @@
  15.119  
  15.120    \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
  15.121    \indexisarelem{defines}\indexisarelem{notes}
  15.122 -  @{rail "
  15.123 +  @{rail \<open>
  15.124      @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
  15.125      ;
  15.126      @@{command print_locale} '!'? @{syntax nameref}
  15.127 @@ -492,12 +492,12 @@
  15.128        @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
  15.129      ;
  15.130      @{syntax_def context_elem}:
  15.131 -      @'fixes' (@{syntax \"fixes\"} + @'and') |
  15.132 +      @'fixes' (@{syntax "fixes"} + @'and') |
  15.133        @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
  15.134        @'assumes' (@{syntax props} + @'and') |
  15.135        @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
  15.136        @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
  15.137 -  "}
  15.138 +  \<close>}
  15.139  
  15.140    \begin{description}
  15.141    
  15.142 @@ -630,7 +630,7 @@
  15.143    "interpretation"}) and also within proof bodies (@{command
  15.144    "interpret"}).
  15.145  
  15.146 -  @{rail "
  15.147 +  @{rail \<open>
  15.148      @@{command interpretation} @{syntax locale_expr} equations?
  15.149      ;
  15.150      @@{command interpret} @{syntax locale_expr} equations?
  15.151 @@ -644,7 +644,7 @@
  15.152      ;
  15.153  
  15.154      equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
  15.155 -  "}
  15.156 +  \<close>}
  15.157  
  15.158    \begin{description}
  15.159  
  15.160 @@ -796,7 +796,7 @@
  15.161    (notably type-inference).  See \cite{isabelle-classes} for a short
  15.162    tutorial.
  15.163  
  15.164 -  @{rail "
  15.165 +  @{rail \<open>
  15.166      @@{command class} class_spec @'begin'?
  15.167      ;
  15.168      class_spec: @{syntax name} '='
  15.169 @@ -809,7 +809,7 @@
  15.170        @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
  15.171      ;
  15.172      @@{command subclass} @{syntax target}? @{syntax nameref}
  15.173 -  "}
  15.174 +  \<close>}
  15.175  
  15.176    \begin{description}
  15.177  
  15.178 @@ -968,11 +968,11 @@
  15.179    The @{command "overloading"} target provides a convenient view for
  15.180    end-users.
  15.181  
  15.182 -  @{rail "
  15.183 +  @{rail \<open>
  15.184      @@{command overloading} ( spec + ) @'begin'
  15.185      ;
  15.186      spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
  15.187 -  "}
  15.188 +  \<close>}
  15.189  
  15.190    \begin{description}
  15.191  
  15.192 @@ -1010,14 +1010,14 @@
  15.193      @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
  15.194    \end{matharray}
  15.195  
  15.196 -  @{rail "
  15.197 +  @{rail \<open>
  15.198      @@{command ML_file} @{syntax name}
  15.199      ;
  15.200      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
  15.201        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
  15.202      ;
  15.203      @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
  15.204 -  "}
  15.205 +  \<close>}
  15.206  
  15.207    \begin{description}
  15.208  
  15.209 @@ -1094,13 +1094,13 @@
  15.210      @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
  15.211    \end{matharray}
  15.212  
  15.213 -  @{rail "
  15.214 +  @{rail \<open>
  15.215      @@{command classes} (@{syntax classdecl} +)
  15.216      ;
  15.217      @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
  15.218      ;
  15.219      @@{command default_sort} @{syntax sort}
  15.220 -  "}
  15.221 +  \<close>}
  15.222  
  15.223    \begin{description}
  15.224  
  15.225 @@ -1141,13 +1141,13 @@
  15.226      @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
  15.227    \end{matharray}
  15.228  
  15.229 -  @{rail "
  15.230 +  @{rail \<open>
  15.231      @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
  15.232      ;
  15.233      @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
  15.234      ;
  15.235      @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
  15.236 -  "}
  15.237 +  \<close>}
  15.238  
  15.239    \begin{description}
  15.240  
  15.241 @@ -1219,13 +1219,13 @@
  15.242    corresponding occurrences on some right-hand side need to be an
  15.243    instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
  15.244  
  15.245 -  @{rail "
  15.246 +  @{rail \<open>
  15.247      @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
  15.248      ;
  15.249      @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
  15.250      ;
  15.251      opt: '(' @'unchecked'? @'overloaded'? ')'
  15.252 -  "}
  15.253 +  \<close>}
  15.254  
  15.255    \begin{description}
  15.256  
  15.257 @@ -1259,11 +1259,11 @@
  15.258      @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
  15.259    \end{matharray}
  15.260  
  15.261 -  @{rail "
  15.262 +  @{rail \<open>
  15.263      (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
  15.264        (@{syntax thmdef}? @{syntax thmrefs} + @'and')
  15.265        (@'for' (@{syntax vars} + @'and'))?
  15.266 -  "}
  15.267 +  \<close>}
  15.268  
  15.269    \begin{description}
  15.270    
  15.271 @@ -1302,9 +1302,9 @@
  15.272    asserted, and records within the internal derivation object how
  15.273    presumed theorems depend on unproven suppositions.
  15.274  
  15.275 -  @{rail "
  15.276 +  @{rail \<open>
  15.277      @@{command oracle} @{syntax name} '=' @{syntax text}
  15.278 -  "}
  15.279 +  \<close>}
  15.280  
  15.281    \begin{description}
  15.282  
  15.283 @@ -1333,10 +1333,10 @@
  15.284      @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
  15.285    \end{matharray}
  15.286  
  15.287 -  @{rail "
  15.288 +  @{rail \<open>
  15.289      ( @{command hide_class} | @{command hide_type} |
  15.290        @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
  15.291 -  "}
  15.292 +  \<close>}
  15.293  
  15.294    Isabelle organizes any kind of name declarations (of types,
  15.295    constants, theorems etc.) by separate hierarchically structured name
    16.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Wed Jan 22 10:13:40 2014 +0100
    16.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Wed Jan 22 17:14:27 2014 +0100
    16.3 @@ -52,7 +52,7 @@
    16.4        end
    16.5    in
    16.6      Thy_Output.antiquotation @{binding "const_typ"}
    16.7 -     (Scan.lift Args.name_source)
    16.8 +     (Scan.lift Args.name_inner_syntax)
    16.9         (fn {source = src, context = ctxt, ...} => fn arg =>
   16.10            Thy_Output.output ctxt
   16.11              (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
    17.1 --- a/src/Doc/System/Sessions.thy	Wed Jan 22 10:13:40 2014 +0100
    17.2 +++ b/src/Doc/System/Sessions.thy	Wed Jan 22 17:14:27 2014 +0100
    17.3 @@ -48,7 +48,7 @@
    17.4    mode @{verbatim "isabelle-root"} for session ROOT files, which is
    17.5    enabled by default for any file of that name.
    17.6  
    17.7 -  @{rail "
    17.8 +  @{rail \<open>
    17.9      @{syntax_def session_chapter}: @'chapter' @{syntax name}
   17.10      ;
   17.11  
   17.12 @@ -73,7 +73,7 @@
   17.13      theories: @'theories' opts? ( @{syntax name} * )
   17.14      ;
   17.15      files: @'files' ( @{syntax name} + )
   17.16 -    "}
   17.17 +  \<close>}
   17.18  
   17.19    \begin{description}
   17.20  
    18.1 --- a/src/Doc/ZF/ZF_Isar.thy	Wed Jan 22 10:13:40 2014 +0100
    18.2 +++ b/src/Doc/ZF/ZF_Isar.thy	Wed Jan 22 17:14:27 2014 +0100
    18.3 @@ -24,9 +24,9 @@
    18.4      @{attribute_def (ZF) TC} & : & @{text attribute} \\
    18.5    \end{matharray}
    18.6  
    18.7 -  @{rail "
    18.8 +  @{rail \<open>
    18.9      @@{attribute (ZF) TC} (() | 'add' | 'del')
   18.10 -  "}
   18.11 +  \<close>}
   18.12  
   18.13    \begin{description}
   18.14    
   18.15 @@ -59,7 +59,7 @@
   18.16      @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
   18.17    \end{matharray}
   18.18  
   18.19 -  @{rail "
   18.20 +  @{rail \<open>
   18.21      (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
   18.22      ;
   18.23  
   18.24 @@ -67,22 +67,22 @@
   18.25      ;
   18.26      intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
   18.27      ;
   18.28 -    hints: @{syntax (ZF) \"monos\"}? condefs? \<newline>
   18.29 +    hints: @{syntax (ZF) "monos"}? condefs? \<newline>
   18.30        @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
   18.31      ;
   18.32 -    @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
   18.33 +    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs}
   18.34      ;
   18.35      condefs: @'con_defs' @{syntax thmrefs}
   18.36      ;
   18.37      @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
   18.38      ;
   18.39      @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
   18.40 -  "}
   18.41 +  \<close>}
   18.42  
   18.43    In the following syntax specification @{text "monos"}, @{text
   18.44    typeintros}, and @{text typeelims} are the same as above.
   18.45  
   18.46 -  @{rail "
   18.47 +  @{rail \<open>
   18.48      (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
   18.49      ;
   18.50  
   18.51 @@ -92,8 +92,8 @@
   18.52      ;
   18.53      con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
   18.54      ;
   18.55 -    hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
   18.56 -  "}
   18.57 +    hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
   18.58 +  \<close>}
   18.59  
   18.60    See \cite{isabelle-ZF} for further information on inductive
   18.61    definitions in ZF, but note that this covers the old-style theory
   18.62 @@ -108,9 +108,9 @@
   18.63      @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
   18.64    \end{matharray}
   18.65  
   18.66 -  @{rail "
   18.67 +  @{rail \<open>
   18.68      @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
   18.69 -  "}
   18.70 +  \<close>}
   18.71  *}
   18.72  
   18.73  
   18.74 @@ -127,14 +127,13 @@
   18.75      @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
   18.76    \end{matharray}
   18.77  
   18.78 -  @{rail "
   18.79 +  @{rail \<open>
   18.80      (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
   18.81      ;
   18.82      @@{method (ZF) ind_cases} (@{syntax prop} +)
   18.83      ;
   18.84      @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
   18.85 -    ;
   18.86 -  "}
   18.87 +  \<close>}
   18.88  *}
   18.89  
   18.90  end
    19.1 --- a/src/FOL/FOL.thy	Wed Jan 22 10:13:40 2014 +0100
    19.2 +++ b/src/FOL/FOL.thy	Wed Jan 22 17:14:27 2014 +0100
    19.3 @@ -72,7 +72,7 @@
    19.4  *}
    19.5  
    19.6  method_setup case_tac = {*
    19.7 -  Args.goal_spec -- Scan.lift Args.name_source >>
    19.8 +  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
    19.9      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
   19.10  *} "case_tac emulation (dynamic instantiation!)"
   19.11  
    20.1 --- a/src/HOL/Library/LaTeXsugar.thy	Wed Jan 22 10:13:40 2014 +0100
    20.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jan 22 17:14:27 2014 +0100
    20.3 @@ -106,7 +106,7 @@
    20.4        end
    20.5    in
    20.6      Thy_Output.antiquotation @{binding "const_typ"}
    20.7 -     (Scan.lift Args.name_source)
    20.8 +     (Scan.lift Args.name_inner_syntax)
    20.9         (fn {source = src, context = ctxt, ...} => fn arg =>
   20.10            Thy_Output.output ctxt
   20.11              (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
    21.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Wed Jan 22 10:13:40 2014 +0100
    21.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Wed Jan 22 17:14:27 2014 +0100
    21.3 @@ -205,7 +205,7 @@
    21.4  val any_line = whitespace' |-- any_line' --|
    21.5    newline >> (implode o map symbol);
    21.6  
    21.7 -fun gen_comment a b = $$$ a |-- !!! "missing end of comment"
    21.8 +fun gen_comment a b = $$$ a |-- !!! "unclosed comment"
    21.9    (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment;
   21.10  
   21.11  val c_comment = gen_comment "/*" "*/";
    22.1 --- a/src/HOL/Tools/inductive.ML	Wed Jan 22 10:13:40 2014 +0100
    22.2 +++ b/src/HOL/Tools/inductive.ML	Wed Jan 22 17:14:27 2014 +0100
    22.3 @@ -591,7 +591,7 @@
    22.4  
    22.5  val ind_cases_setup =
    22.6    Method.setup @{binding ind_cases}
    22.7 -    (Scan.lift (Scan.repeat1 Args.name_source --
    22.8 +    (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
    22.9        Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
   22.10        (fn (raw_props, fixes) => fn ctxt =>
   22.11          let
    23.1 --- a/src/HOL/Tools/string_syntax.ML	Wed Jan 22 10:13:40 2014 +0100
    23.2 +++ b/src/HOL/Tools/string_syntax.ML	Wed Jan 22 17:14:27 2014 +0100
    23.3 @@ -38,24 +38,24 @@
    23.4  val specials = raw_explode "\\\"`'";
    23.5  
    23.6  fun dest_chr c1 c2 =
    23.7 -  let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
    23.8 -    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
    23.9 -    then c
   23.10 -    else if c = "\n" then "\<newline>"
   23.11 +  let val s = chr (dest_nib c1 * 16 + dest_nib c2) in
   23.12 +    if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
   23.13 +    then s
   23.14 +    else if s = "\n" then "\<newline>"
   23.15      else raise Match
   23.16    end;
   23.17  
   23.18  fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   23.19    | dest_char _ = raise Match;
   23.20  
   23.21 -fun syntax_string cs =
   23.22 +fun syntax_string ss =
   23.23    Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
   23.24 -    Ast.Variable (Lexicon.implode_str cs)];
   23.25 +    Ast.Variable (Lexicon.implode_str ss)];
   23.26  
   23.27  
   23.28  fun char_ast_tr [Ast.Variable str] =
   23.29 -      (case Lexicon.explode_str str of
   23.30 -        [c] => mk_char c
   23.31 +      (case Lexicon.explode_str (str, Position.none) of
   23.32 +        [(s, _)] => mk_char s
   23.33        | _ => error ("Single character expected: " ^ str))
   23.34    | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
   23.35        Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
   23.36 @@ -69,16 +69,16 @@
   23.37  (* string *)
   23.38  
   23.39  fun mk_string [] = Ast.Constant @{const_syntax Nil}
   23.40 -  | mk_string (c :: cs) =
   23.41 -      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
   23.42 +  | mk_string (s :: ss) =
   23.43 +      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss];
   23.44  
   23.45  fun string_ast_tr [Ast.Variable str] =
   23.46 -      (case Lexicon.explode_str str of
   23.47 +      (case Lexicon.explode_str (str, Position.none) of
   23.48          [] =>
   23.49            Ast.Appl
   23.50              [Ast.Constant @{syntax_const "_constrain"},
   23.51                Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
   23.52 -      | cs => mk_string cs)
   23.53 +      | ss => mk_string (map Symbol_Pos.symbol ss))
   23.54    | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
   23.55        Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
   23.56    | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
    24.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Wed Jan 22 10:13:40 2014 +0100
    24.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Jan 22 17:14:27 2014 +0100
    24.3 @@ -16,7 +16,7 @@
    24.4      "for proving safety properties"
    24.5  
    24.6  method_setup ensures_tac = {*
    24.7 -  Args.goal_spec -- Scan.lift Args.name_source >>
    24.8 +  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
    24.9    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
   24.10  *} "for proving progress properties"
   24.11  
    25.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Jan 22 10:13:40 2014 +0100
    25.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Jan 22 17:14:27 2014 +0100
    25.3 @@ -2,10 +2,12 @@
    25.4  
    25.5  theory Cartouche_Examples
    25.6  imports Main
    25.7 -keywords "cartouche" :: diag
    25.8 +keywords
    25.9 +  "cartouche" "term_cartouche" :: diag and
   25.10 +  "text_cartouche" :: thy_decl
   25.11  begin
   25.12  
   25.13 -subsection {* Outer syntax *}
   25.14 +subsection {* Outer syntax: cartouche within command syntax *}
   25.15  
   25.16  ML {*
   25.17    Outer_Syntax.improper_command @{command_spec "cartouche"} ""
   25.18 @@ -17,12 +19,10 @@
   25.19  cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close>
   25.20  
   25.21  
   25.22 -subsection {* Inner syntax *}
   25.23 +subsection {* Inner syntax: string literals via cartouche *}
   25.24  
   25.25 -syntax "_string_cartouche" :: "cartouche_position \<Rightarrow> string"  ("STR _")
   25.26 -
   25.27 -parse_translation {*
   25.28 -  let
   25.29 +ML {*
   25.30 +  local
   25.31      val mk_nib =
   25.32        Syntax.const o Lexicon.mark_const o
   25.33          fst o Term.dest_Const o HOLogic.mk_nibble;
   25.34 @@ -39,27 +39,139 @@
   25.35        | mk_string (s :: ss) =
   25.36            Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss;
   25.37  
   25.38 -    fun string_tr ctxt args =
   25.39 -      let fun err () = raise TERM ("string_tr", []) in
   25.40 +  in
   25.41 +    fun string_tr content args =
   25.42 +      let fun err () = raise TERM ("string_tr", args) in
   25.43          (case args of
   25.44            [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
   25.45              (case Term_Position.decode_position p of
   25.46 -              SOME (pos, _) =>
   25.47 -                c $ mk_string (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))) $ p
   25.48 +              SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
   25.49              | NONE => err ())
   25.50          | _ => err ())
   25.51        end;
   25.52 -  in
   25.53 -    [(@{syntax_const "_string_cartouche"}, string_tr)]
   25.54 -  end
   25.55 +  end;
   25.56 +*}
   25.57 +
   25.58 +syntax "_STR_cartouche" :: "cartouche_position \<Rightarrow> string"  ("STR _")
   25.59 +
   25.60 +parse_translation {*
   25.61 +  [(@{syntax_const "_STR_cartouche"},
   25.62 +    K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
   25.63  *}
   25.64  
   25.65  term "STR \<open>\<close>"
   25.66  term "STR \<open>abc\<close>"
   25.67 -lemma "STR \<open>abc\<close> @ STR \<open>xyz\<close> = STR \<open>abcxyz\<close>" by simp
   25.68 +term "STR \<open>abc\<close> @ STR \<open>xyz\<close>"
   25.69 +term "STR \<open>\<newline>\<close>"
   25.70 +term "STR \<open>\001\010\100\<close>"
   25.71 +
   25.72 +
   25.73 +subsection {* Alternate outer and inner syntax: string literals *}
   25.74 +
   25.75 +subsubsection {* Nested quotes *}
   25.76 +
   25.77 +syntax "_STR_string" :: "string_position \<Rightarrow> string"  ("STR _")
   25.78 +
   25.79 +parse_translation {*
   25.80 +  [(@{syntax_const "_STR_string"}, K (string_tr Lexicon.explode_string))]
   25.81 +*}
   25.82 +
   25.83 +term "STR \"\""
   25.84 +term "STR \"abc\""
   25.85 +term "STR \"abc\" @ STR \"xyz\""
   25.86 +term "STR \"\<newline>\""
   25.87 +term "STR \"\001\010\100\""
   25.88 +
   25.89 +
   25.90 +subsubsection {* Term cartouche and regular quotes *}
   25.91 +
   25.92 +ML {*
   25.93 +  Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
   25.94 +    (Parse.inner_syntax Parse.cartouche >> (fn s =>
   25.95 +      Toplevel.keep (fn state =>
   25.96 +        let
   25.97 +          val ctxt = Toplevel.context_of state;
   25.98 +          val t = Syntax.read_term ctxt s;
   25.99 +        in writeln (Syntax.string_of_term ctxt t) end)))
  25.100 +*}
  25.101 +
  25.102 +term_cartouche \<open>STR ""\<close>
  25.103 +term_cartouche \<open>STR "abc"\<close>
  25.104 +term_cartouche \<open>STR "abc" @ STR "xyz"\<close>
  25.105 +term_cartouche \<open>STR "\<newline>"\<close>
  25.106 +term_cartouche \<open>STR "\001\010\100"\<close>
  25.107  
  25.108  
  25.109 -subsection {* Proof method syntax *}
  25.110 +subsubsection {* Further nesting: antiquotations *}
  25.111 +
  25.112 +setup -- "ML antiquotation"
  25.113 +{*
  25.114 +  ML_Antiquote.inline @{binding term_cartouche}
  25.115 +    (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
  25.116 +      (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
  25.117 +*}
  25.118 +
  25.119 +setup -- "document antiquotation"
  25.120 +{*
  25.121 +  Thy_Output.antiquotation @{binding ML_cartouche}
  25.122 +    (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn (txt, pos) =>
  25.123 +      let
  25.124 +        val toks =
  25.125 +          ML_Lex.read Position.none "fn _ => (" @
  25.126 +          ML_Lex.read pos txt @
  25.127 +          ML_Lex.read Position.none ");";
  25.128 +        val _ = ML_Context.eval_in (SOME context) false pos toks;
  25.129 +      in "" end);
  25.130 +*}
  25.131 +
  25.132 +ML {*
  25.133 +  @{term_cartouche \<open>STR ""\<close>};
  25.134 +  @{term_cartouche \<open>STR "abc"\<close>};
  25.135 +  @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
  25.136 +  @{term_cartouche \<open>STR "\<newline>"\<close>};
  25.137 +  @{term_cartouche \<open>STR "\001\010\100"\<close>};
  25.138 +*}
  25.139 +
  25.140 +text {*
  25.141 +  @{ML_cartouche
  25.142 +    \<open>
  25.143 +      (
  25.144 +        @{term_cartouche \<open>STR ""\<close>};
  25.145 +        @{term_cartouche \<open>STR "abc"\<close>};
  25.146 +        @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
  25.147 +        @{term_cartouche \<open>STR "\<newline>"\<close>};
  25.148 +        @{term_cartouche \<open>STR "\001\010\100"\<close>}
  25.149 +      )
  25.150 +    \<close>
  25.151 +  }
  25.152 +*}
  25.153 +
  25.154 +
  25.155 +subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *}
  25.156 +
  25.157 +ML {*
  25.158 +  Outer_Syntax.command
  25.159 +    @{command_spec "text_cartouche"} ""
  25.160 +    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup)
  25.161 +*}
  25.162 +
  25.163 +text_cartouche
  25.164 +\<open>
  25.165 +  @{ML_cartouche
  25.166 +    \<open>
  25.167 +      (
  25.168 +        @{term_cartouche \<open>STR ""\<close>};
  25.169 +        @{term_cartouche \<open>STR "abc"\<close>};
  25.170 +        @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
  25.171 +        @{term_cartouche \<open>STR "\<newline>"\<close>};
  25.172 +        @{term_cartouche \<open>STR "\001\010\100"\<close>}
  25.173 +      )
  25.174 +    \<close>
  25.175 +  }
  25.176 +\<close>
  25.177 +
  25.178 +
  25.179 +subsection {* Proof method syntax: ML tactic expression *}
  25.180  
  25.181  ML {*
  25.182  structure ML_Tactic:
  25.183 @@ -83,7 +195,7 @@
  25.184  *}
  25.185  
  25.186  
  25.187 -subsection {* Explicit version: method with cartouche argument *}
  25.188 +subsubsection {* Explicit version: method with cartouche argument *}
  25.189  
  25.190  method_setup ml_tactic = {*
  25.191    Scan.lift Args.cartouche_source_position
  25.192 @@ -104,7 +216,7 @@
  25.193  text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *}
  25.194  
  25.195  
  25.196 -subsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
  25.197 +subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
  25.198  
  25.199  method_setup "cartouche" = {*
  25.200    Scan.lift Args.cartouche_source_position
    26.1 --- a/src/Pure/General/antiquote.ML	Wed Jan 22 10:13:40 2014 +0100
    26.2 +++ b/src/Pure/General/antiquote.ML	Wed Jan 22 17:14:27 2014 +0100
    26.3 @@ -45,20 +45,20 @@
    26.4  val err_prefix = "Antiquotation lexical error: ";
    26.5  
    26.6  val scan_txt =
    26.7 -  $$$ "@" --| Scan.ahead (~$$$ "{") ||
    26.8 +  $$$ "@" --| Scan.ahead (~$$ "{") ||
    26.9    Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
   26.10  
   26.11  val scan_ant =
   26.12    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   26.13 -  Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 ||
   26.14 +  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
   26.15    Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
   26.16  
   26.17  in
   26.18  
   26.19  val scan_antiq =
   26.20 -  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
   26.21 +  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
   26.22      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
   26.23 -      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
   26.24 +      (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
   26.25    >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
   26.26  
   26.27  val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
    27.1 --- a/src/Pure/General/scan.ML	Wed Jan 22 10:13:40 2014 +0100
    27.2 +++ b/src/Pure/General/scan.ML	Wed Jan 22 17:14:27 2014 +0100
    27.3 @@ -64,6 +64,7 @@
    27.4    val state: 'a * 'b -> 'a * ('a * 'b)
    27.5    val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
    27.6    val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
    27.7 +  val provide: ('a -> bool) -> 'b -> ('b * 'c -> 'd * ('a * 'e)) -> 'c -> 'd * 'e
    27.8    val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
    27.9    val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
   27.10    val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd
   27.11 @@ -210,9 +211,11 @@
   27.12  
   27.13  fun peek scan = depend (fn st => scan st >> pair st);
   27.14  
   27.15 -fun pass st scan xs =
   27.16 -  let val (y, (_, xs')) = scan (st, xs)
   27.17 -  in (y, xs') end;
   27.18 +fun provide pred st scan xs =
   27.19 +  let val (y, (st', xs')) = scan (st, xs)
   27.20 +  in if pred st' then (y, xs') else fail () end;
   27.21 +
   27.22 +fun pass st = provide (K true) st;
   27.23  
   27.24  fun lift scan (st, xs) =
   27.25    let val (y, xs') = scan xs
    28.1 --- a/src/Pure/General/symbol_pos.ML	Wed Jan 22 10:13:40 2014 +0100
    28.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Jan 22 17:14:27 2014 +0100
    28.3 @@ -8,6 +8,8 @@
    28.4  sig
    28.5    type T = Symbol.symbol * Position.T
    28.6    val symbol: T -> Symbol.symbol
    28.7 +  val $$ : Symbol.symbol -> T list -> T * T list
    28.8 +  val ~$$ : Symbol.symbol -> T list -> T * T list
    28.9    val $$$ : Symbol.symbol -> T list -> T list * T list
   28.10    val ~$$$ : Symbol.symbol -> T list -> T list * T list
   28.11    val content: T list -> string
   28.12 @@ -26,16 +28,11 @@
   28.13    val quote_string_q: string -> string
   28.14    val quote_string_qq: string -> string
   28.15    val quote_string_bq: string -> string
   28.16 -  val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   28.17 -    T list -> T list * T list
   28.18 -  val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   28.19 -    T list -> T list * T list
   28.20 +  val scan_cartouche: string -> T list -> T list * T list
   28.21    val recover_cartouche: T list -> T list * T list
   28.22    val cartouche_content: T list -> T list
   28.23 -  val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   28.24 -    T list -> T list * T list
   28.25 -  val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   28.26 -    T list -> T list * T list
   28.27 +  val scan_comment: string -> T list -> T list * T list
   28.28 +  val scan_comment_body: string -> T list -> T list * T list
   28.29    val recover_comment: T list -> T list * T list
   28.30    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
   28.31      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   28.32 @@ -91,6 +88,8 @@
   28.33  fun change_prompt scan = Scan.prompt "# " scan;
   28.34  
   28.35  fun $$ s = Scan.one (fn x => symbol x = s);
   28.36 +fun ~$$ s = Scan.one (fn x => symbol x <> s);
   28.37 +
   28.38  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
   28.39  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
   28.40  
   28.41 @@ -115,8 +114,10 @@
   28.42    Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
   28.43  
   28.44  fun scan_strs q err_prefix =
   28.45 -  (scan_pos --| $$$ q) -- !!! (fn () => err_prefix ^ "missing quote at end of string")
   28.46 -    (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
   28.47 +  Scan.ahead ($$ q) |--
   28.48 +    !!! (fn () => err_prefix ^ "unclosed string literal")
   28.49 +      ((scan_pos --| $$$ q) --
   28.50 +        (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))));
   28.51  
   28.52  fun recover_strs q =
   28.53    $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
   28.54 @@ -159,29 +160,20 @@
   28.55  
   28.56  (* nested text cartouches *)
   28.57  
   28.58 -local
   28.59 -
   28.60 -val scan_cart =
   28.61 -  Scan.depend (fn (d: int) => $$ "\\<open>" >> pair (d + 1)) ||
   28.62 -  Scan.depend (fn 0 => Scan.fail | d => $$ "\\<close>" >> pair (d - 1)) ||
   28.63 -  Scan.lift (Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s));
   28.64 -
   28.65 -val scan_carts = Scan.pass 0 (Scan.repeat scan_cart);
   28.66 -
   28.67 -val scan_body = change_prompt scan_carts;
   28.68 +val scan_cartouche_depth =
   28.69 +  Scan.repeat1 (Scan.depend (fn (d: int) =>
   28.70 +    $$ "\\<open>" >> pair (d + 1) ||
   28.71 +      (if d > 0 then
   28.72 +        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
   28.73 +        $$ "\\<close>" >> pair (d - 1)
   28.74 +      else Scan.fail)));
   28.75  
   28.76 -in
   28.77 -
   28.78 -fun scan_cartouche cut =
   28.79 -  $$ "\\<open>" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\<close>");
   28.80 +fun scan_cartouche err_prefix =
   28.81 +  Scan.ahead ($$ "\\<open>") |--
   28.82 +    !!! (fn () => err_prefix ^ "unclosed text cartouche")
   28.83 +      (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
   28.84  
   28.85 -fun scan_cartouche_body cut =
   28.86 -  $$ "\\<open>" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\<close>");
   28.87 -
   28.88 -val recover_cartouche =
   28.89 -  $$$ "\\<open>" @@@ scan_carts;
   28.90 -
   28.91 -end;
   28.92 +val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
   28.93  
   28.94  fun cartouche_content syms =
   28.95    let
   28.96 @@ -214,11 +206,15 @@
   28.97  
   28.98  in
   28.99  
  28.100 -fun scan_comment cut =
  28.101 -  $$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")");
  28.102 +fun scan_comment err_prefix =
  28.103 +  Scan.ahead ($$ "(" -- $$ "*") |--
  28.104 +    !!! (fn () => err_prefix ^ "unclosed comment")
  28.105 +      ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
  28.106  
  28.107 -fun scan_comment_body cut =
  28.108 -  $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")");
  28.109 +fun scan_comment_body err_prefix =
  28.110 +  Scan.ahead ($$ "(" -- $$ "*") |--
  28.111 +    !!! (fn () => err_prefix ^ "unclosed comment")
  28.112 +      ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
  28.113  
  28.114  val recover_comment =
  28.115    $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
  28.116 @@ -284,6 +280,8 @@
  28.117  
  28.118  structure Basic_Symbol_Pos =   (*not open by default*)
  28.119  struct
  28.120 +  val $$ = Symbol_Pos.$$;
  28.121 +  val ~$$ = Symbol_Pos.~$$;
  28.122    val $$$ = Symbol_Pos.$$$;
  28.123    val ~$$$ = Symbol_Pos.~$$$;
  28.124  end;
    29.1 --- a/src/Pure/Isar/args.ML	Wed Jan 22 10:13:40 2014 +0100
    29.2 +++ b/src/Pure/Isar/args.ML	Wed Jan 22 17:14:27 2014 +0100
    29.3 @@ -29,9 +29,9 @@
    29.4    val bracks: 'a parser -> 'a parser
    29.5    val mode: string -> bool parser
    29.6    val maybe: 'a parser -> 'a option parser
    29.7 -  val cartouche_source: string parser
    29.8 +  val cartouche_inner_syntax: string parser
    29.9    val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
   29.10 -  val name_source: string parser
   29.11 +  val name_inner_syntax: string parser
   29.12    val name_source_position: (Symbol_Pos.text * Position.T) parser
   29.13    val name: string parser
   29.14    val binding: binding parser
   29.15 @@ -151,10 +151,10 @@
   29.16  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
   29.17  
   29.18  val cartouche = token Parse.cartouche;
   29.19 -val cartouche_source = cartouche >> Token.source_of;
   29.20 +val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
   29.21  val cartouche_source_position = cartouche >> Token.source_position_of;
   29.22  
   29.23 -val name_source = named >> Token.source_of;
   29.24 +val name_inner_syntax = named >> Token.inner_syntax_of;
   29.25  val name_source_position = named >> Token.source_position_of;
   29.26  
   29.27  val name = named >> Token.content_of;
   29.28 @@ -182,11 +182,11 @@
   29.29  val internal_attribute = value (fn Token.Attribute att => att);
   29.30  
   29.31  fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
   29.32 -fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
   29.33 -fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
   29.34 +fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
   29.35 +fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
   29.36  
   29.37  fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
   29.38 -  alt_string >> evaluate Token.Fact (get o Token.source_of);
   29.39 +  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
   29.40  
   29.41  fun named_attribute att =
   29.42    internal_attribute ||
    30.1 --- a/src/Pure/Isar/parse.ML	Wed Jan 22 10:13:40 2014 +0100
    30.2 +++ b/src/Pure/Isar/parse.ML	Wed Jan 22 17:14:27 2014 +0100
    30.3 @@ -167,7 +167,7 @@
    30.4  
    30.5  fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
    30.6  fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
    30.7 -fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
    30.8 +fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
    30.9  
   30.10  fun kind k =
   30.11    group (fn () => Token.str_of_kind k)
    31.1 --- a/src/Pure/Isar/token.ML	Wed Jan 22 10:13:40 2014 +0100
    31.2 +++ b/src/Pure/Isar/token.ML	Wed Jan 22 17:14:27 2014 +0100
    31.3 @@ -41,7 +41,7 @@
    31.4    val is_space: T -> bool
    31.5    val is_blank: T -> bool
    31.6    val is_newline: T -> bool
    31.7 -  val source_of: T -> string
    31.8 +  val inner_syntax_of: T -> string
    31.9    val source_position_of: T -> Symbol_Pos.text * Position.T
   31.10    val content_of: T -> string
   31.11    val unparse: T -> string
   31.12 @@ -116,10 +116,10 @@
   31.13    | TypeVar => "schematic type variable"
   31.14    | Nat => "natural number"
   31.15    | Float => "floating-point number"
   31.16 -  | String => "string"
   31.17 +  | String => "quoted string"
   31.18    | AltString => "back-quoted string"
   31.19    | Verbatim => "verbatim text"
   31.20 -  | Cartouche => "cartouche"
   31.21 +  | Cartouche => "text cartouche"
   31.22    | Space => "white space"
   31.23    | Comment => "comment text"
   31.24    | InternalValue => "internal value"
   31.25 @@ -206,7 +206,7 @@
   31.26  
   31.27  (* token content *)
   31.28  
   31.29 -fun source_of (Token ((source, (pos, _)), (_, x), _)) =
   31.30 +fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
   31.31    if YXML.detect x then x
   31.32    else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
   31.33  
   31.34 @@ -321,13 +321,15 @@
   31.35  (* scan verbatim text *)
   31.36  
   31.37  val scan_verb =
   31.38 -  $$$ "*" --| Scan.ahead (~$$$ "}") ||
   31.39 +  $$$ "*" --| Scan.ahead (~$$ "}") ||
   31.40    Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
   31.41  
   31.42  val scan_verbatim =
   31.43 -  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
   31.44 -    (Symbol_Pos.change_prompt
   31.45 -      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
   31.46 +  Scan.ahead ($$ "{" -- $$ "*") |--
   31.47 +    !!! "unclosed verbatim text"
   31.48 +      ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
   31.49 +        Symbol_Pos.change_prompt
   31.50 +          ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
   31.51  
   31.52  val recover_verbatim =
   31.53    $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
   31.54 @@ -336,7 +338,8 @@
   31.55  (* scan cartouche *)
   31.56  
   31.57  val scan_cartouche =
   31.58 -  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos);
   31.59 +  Symbol_Pos.scan_pos --
   31.60 +    ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
   31.61  
   31.62  
   31.63  (* scan space *)
   31.64 @@ -351,7 +354,7 @@
   31.65  (* scan comment *)
   31.66  
   31.67  val scan_comment =
   31.68 -  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
   31.69 +  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos);
   31.70  
   31.71  
   31.72  
    32.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Jan 22 10:13:40 2014 +0100
    32.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Jan 22 17:14:27 2014 +0100
    32.3 @@ -99,14 +99,14 @@
    32.4  
    32.5    value (Binding.name "cpat")
    32.6      (Args.context --
    32.7 -      Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
    32.8 +      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
    32.9          "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   32.10            ML_Syntax.atomic (ML_Syntax.print_term t))));
   32.11  
   32.12  
   32.13  (* type classes *)
   32.14  
   32.15 -fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   32.16 +fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   32.17    Proof_Context.read_class ctxt s
   32.18    |> syn ? Lexicon.mark_class
   32.19    |> ML_Syntax.print_string);
   32.20 @@ -116,13 +116,13 @@
   32.21    inline (Binding.name "class_syntax") (class true) #>
   32.22  
   32.23    inline (Binding.name "sort")
   32.24 -    (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   32.25 +    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   32.26        ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   32.27  
   32.28  
   32.29  (* type constructors *)
   32.30  
   32.31 -fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
   32.32 +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   32.33    >> (fn (ctxt, (s, pos)) =>
   32.34      let
   32.35        val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
   32.36 @@ -146,7 +146,7 @@
   32.37  
   32.38  (* constants *)
   32.39  
   32.40 -fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
   32.41 +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   32.42    >> (fn (ctxt, (s, pos)) =>
   32.43      let
   32.44        val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
   32.45 @@ -169,7 +169,7 @@
   32.46        else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   32.47  
   32.48    inline (Binding.name "const")
   32.49 -    (Args.context -- Scan.lift Args.name_source -- Scan.optional
   32.50 +    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
   32.51          (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   32.52        >> (fn ((ctxt, raw_c), Ts) =>
   32.53          let
    33.1 --- a/src/Pure/ML/ml_lex.ML	Wed Jan 22 10:13:40 2014 +0100
    33.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Jan 22 17:14:27 2014 +0100
    33.3 @@ -137,7 +137,9 @@
    33.4  
    33.5  open Basic_Symbol_Pos;
    33.6  
    33.7 -fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
    33.8 +val err_prefix = "SML lexical error: ";
    33.9 +
   33.10 +fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
   33.11  
   33.12  
   33.13  (* blanks *)
   33.14 @@ -241,8 +243,9 @@
   33.15    $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) [];
   33.16  
   33.17  val scan_string =
   33.18 -  $$$ "\"" @@@ !!! "missing quote at end of string"
   33.19 -    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
   33.20 +  Scan.ahead ($$ "\"") |--
   33.21 +    !!! "unclosed string literal"
   33.22 +      ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
   33.23  
   33.24  val recover_string =
   33.25    $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
   33.26 @@ -260,7 +263,7 @@
   33.27   (scan_char >> token Char ||
   33.28    scan_string >> token String ||
   33.29    scan_blanks1 >> token Space ||
   33.30 -  Symbol_Pos.scan_comment !!! >> token Comment ||
   33.31 +  Symbol_Pos.scan_comment err_prefix >> token Comment ||
   33.32    Scan.max token_leq
   33.33     (scan_keyword >> token Keyword)
   33.34     (scan_word >> token Word ||
   33.35 @@ -304,9 +307,7 @@
   33.36            (SOME (false, fn msg => recover msg >> map Antiquote.Text))
   33.37          |> Source.exhaust
   33.38          |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
   33.39 -        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
   33.40 -      handle ERROR msg =>
   33.41 -        cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
   33.42 +        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
   33.43    in input @ termination end;
   33.44  
   33.45  end;
    34.1 --- a/src/Pure/ML/ml_thms.ML	Wed Jan 22 10:13:40 2014 +0100
    34.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Jan 22 17:14:27 2014 +0100
    34.3 @@ -85,7 +85,7 @@
    34.4  
    34.5  val and_ = Args.$$$ "and";
    34.6  val by = Args.$$$ "by";
    34.7 -val goal = Scan.unless (by || and_) Args.name_source;
    34.8 +val goal = Scan.unless (by || and_) Args.name_inner_syntax;
    34.9  
   34.10  val _ = Theory.setup
   34.11    (ML_Context.add_antiq (Binding.name "lemma")
    35.1 --- a/src/Pure/Syntax/lexicon.ML	Wed Jan 22 10:13:40 2014 +0100
    35.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 22 17:14:27 2014 +0100
    35.3 @@ -24,8 +24,8 @@
    35.4    val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    35.5    val is_tid: string -> bool
    35.6    datatype token_kind =
    35.7 -    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
    35.8 -    NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF
    35.9 +    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
   35.10 +    FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF
   35.11    datatype token = Token of token_kind * string * Position.range
   35.12    val str_of_token: token -> string
   35.13    val pos_of_token: token -> Position.T
   35.14 @@ -42,8 +42,10 @@
   35.15    val matching_tokens: token * token -> bool
   35.16    val valued_token: token -> bool
   35.17    val predef_term: string -> token option
   35.18 -  val implode_str: string list -> string
   35.19 -  val explode_str: string -> string list
   35.20 +  val implode_string: Symbol.symbol list -> string
   35.21 +  val explode_string: string * Position.T -> Symbol_Pos.T list
   35.22 +  val implode_str: Symbol.symbol list -> string
   35.23 +  val explode_str: string * Position.T -> Symbol_Pos.T list
   35.24    val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
   35.25    val read_indexname: string -> indexname
   35.26    val read_var: string -> term
   35.27 @@ -87,7 +89,9 @@
   35.28  
   35.29  open Basic_Symbol_Pos;
   35.30  
   35.31 -fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
   35.32 +val err_prefix = "Inner lexical error: ";
   35.33 +
   35.34 +fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
   35.35  
   35.36  val scan_id = Symbol_Pos.scan_ident;
   35.37  val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
   35.38 @@ -114,8 +118,8 @@
   35.39  (** datatype token **)
   35.40  
   35.41  datatype token_kind =
   35.42 -  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
   35.43 -  NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF;
   35.44 +  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
   35.45 +  FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF;
   35.46  
   35.47  datatype token = Token of token_kind * string * Position.range;
   35.48  
   35.49 @@ -150,6 +154,7 @@
   35.50    ("float_token", FloatSy),
   35.51    ("xnum_token", XNumSy),
   35.52    ("str_token", StrSy),
   35.53 +  ("string_token", StringSy),
   35.54    ("cartouche", Cartouche)];
   35.55  
   35.56  val terminals = map #1 terminal_kinds;
   35.57 @@ -170,6 +175,7 @@
   35.58    | FloatSy => Markup.numeral
   35.59    | XNumSy => Markup.numeral
   35.60    | StrSy => Markup.inner_string
   35.61 +  | StringSy => Markup.inner_string
   35.62    | Cartouche => Markup.inner_cartouche
   35.63    | Comment => Markup.inner_comment
   35.64    | _ => Markup.empty;
   35.65 @@ -205,30 +211,45 @@
   35.66    | NONE => NONE);
   35.67  
   35.68  
   35.69 -(* str tokens *)
   35.70 +
   35.71 +(** string literals **)
   35.72 +
   35.73 +fun explode_literal scan_body (str, pos) =
   35.74 +  (case Scan.read Symbol_Pos.stopper scan_body (Symbol_Pos.explode (str, pos)) of
   35.75 +    SOME ss => ss
   35.76 +  | _ => error (err_prefix ^ "malformed string literal " ^ quote str ^ Position.here pos));
   35.77 +
   35.78 +
   35.79 +(* string *)
   35.80 +
   35.81 +val scan_string = Scan.trace (Symbol_Pos.scan_string_qq err_prefix) >> #2;
   35.82 +val scan_string_body = Symbol_Pos.scan_string_qq err_prefix >> (#1 o #2);
   35.83 +
   35.84 +fun implode_string ss = quote (implode (map (fn "\"" => "\\\"" | s => s) ss));
   35.85 +val explode_string = explode_literal scan_string_body;
   35.86 +
   35.87 +
   35.88 +(* str *)
   35.89  
   35.90  val scan_chr =
   35.91 -  $$$ "\\" |-- $$$ "'" ||
   35.92 +  $$ "\\" |-- $$$ "'" ||
   35.93    Scan.one
   35.94      ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
   35.95        Symbol_Pos.symbol) >> single ||
   35.96 -  $$$ "'" --| Scan.ahead (~$$$ "'");
   35.97 +  $$$ "'" --| Scan.ahead (~$$ "'");
   35.98  
   35.99  val scan_str =
  35.100 -  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
  35.101 -    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
  35.102 +  Scan.ahead ($$ "'" -- $$ "'") |--
  35.103 +    !!! "unclosed string literal"
  35.104 +      ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
  35.105  
  35.106  val scan_str_body =
  35.107 -  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
  35.108 -    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
  35.109 -
  35.110 +  Scan.ahead ($$ "'" |-- $$ "'") |--
  35.111 +    !!! "unclosed string literal"
  35.112 +      ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
  35.113  
  35.114 -fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
  35.115 -
  35.116 -fun explode_str str =
  35.117 -  (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
  35.118 -    SOME cs => map Symbol_Pos.symbol cs
  35.119 -  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
  35.120 +fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss));
  35.121 +val explode_str = explode_literal scan_str_body;
  35.122  
  35.123  
  35.124  
  35.125 @@ -258,17 +279,18 @@
  35.126      val scan_lit = Scan.literal lex >> token Literal;
  35.127  
  35.128      val scan_token =
  35.129 -      Symbol_Pos.scan_cartouche !!! >> token Cartouche ||
  35.130 -      Symbol_Pos.scan_comment !!! >> token Comment ||
  35.131 +      Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
  35.132 +      Symbol_Pos.scan_comment err_prefix >> token Comment ||
  35.133        Scan.max token_leq scan_lit scan_val ||
  35.134 +      scan_string >> token StringSy ||
  35.135        scan_str >> token StrSy ||
  35.136        Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
  35.137    in
  35.138      (case Scan.error
  35.139          (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
  35.140        (toks, []) => toks
  35.141 -    | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
  35.142 -        Position.here (#1 (Symbol_Pos.range ss))))
  35.143 +    | (_, ss) =>
  35.144 +        error (err_prefix ^ Symbol_Pos.content ss ^ Position.here (#1 (Symbol_Pos.range ss))))
  35.145    end;
  35.146  
  35.147  
  35.148 @@ -293,7 +315,7 @@
  35.149  
  35.150      val scan =
  35.151        (scan_id >> map Symbol_Pos.symbol) --
  35.152 -      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
  35.153 +      Scan.optional ($$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
  35.154    in
  35.155      scan >>
  35.156        (fn (cs, ~1) => chop_idx (rev cs) []
  35.157 @@ -302,7 +324,7 @@
  35.158  
  35.159  in
  35.160  
  35.161 -val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
  35.162 +val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
  35.163  
  35.164  end;
  35.165  
  35.166 @@ -320,7 +342,7 @@
  35.167  fun read_var str =
  35.168    let
  35.169      val scan =
  35.170 -      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
  35.171 +      $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
  35.172          >> Syntax.var ||
  35.173        Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
  35.174          >> (Syntax.free o implode o map Symbol_Pos.symbol);
  35.175 @@ -330,7 +352,7 @@
  35.176  (* read_variable *)
  35.177  
  35.178  fun read_variable str =
  35.179 -  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
  35.180 +  let val scan = $$ "?" |-- scan_indexname || scan_indexname
  35.181    in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
  35.182  
  35.183  
    36.1 --- a/src/Pure/Thy/thy_output.ML	Wed Jan 22 10:13:40 2014 +0100
    36.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Jan 22 17:14:27 2014 +0100
    36.3 @@ -570,9 +570,9 @@
    36.4    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
    36.5    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
    36.6    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
    36.7 -  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
    36.8 +  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
    36.9    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   36.10 -  basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
   36.11 +  basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
   36.12    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
   36.13    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
   36.14    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
    37.1 --- a/src/Pure/Tools/rail.ML	Wed Jan 22 10:13:40 2014 +0100
    37.2 +++ b/src/Pure/Tools/rail.ML	Wed Jan 22 17:14:27 2014 +0100
    37.3 @@ -266,7 +266,7 @@
    37.4  
    37.5  val _ = Theory.setup
    37.6    (Thy_Output.antiquotation @{binding rail}
    37.7 -    (Scan.lift (Parse.source_position Parse.string))
    37.8 +    (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
    37.9      (fn {state, ...} => output_rules state o read));
   37.10  
   37.11  end;
    38.1 --- a/src/Pure/Tools/rule_insts.ML	Wed Jan 22 10:13:40 2014 +0100
    38.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Jan 22 17:14:27 2014 +0100
    38.3 @@ -165,7 +165,7 @@
    38.4  
    38.5  val _ = Theory.setup
    38.6    (Attrib.setup @{binding "where"}
    38.7 -    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
    38.8 +    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
    38.9        (fn args =>
   38.10          Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
   38.11      "named instantiation of theorem");
   38.12 @@ -175,7 +175,7 @@
   38.13  
   38.14  local
   38.15  
   38.16 -val inst = Args.maybe Args.name_source;
   38.17 +val inst = Args.maybe Args.name_inner_syntax;
   38.18  val concl = Args.$$$ "concl" -- Args.colon;
   38.19  
   38.20  val insts =
   38.21 @@ -320,7 +320,7 @@
   38.22  fun method inst_tac tac =
   38.23    Args.goal_spec --
   38.24    Scan.optional (Scan.lift
   38.25 -    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
   38.26 +    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --|
   38.27        Args.$$$ "in")) [] --
   38.28    Attrib.thms >>
   38.29    (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
   38.30 @@ -347,12 +347,12 @@
   38.31    Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
   38.32      "cut rule (dynamic instantiation)" #>
   38.33    Method.setup @{binding subgoal_tac}
   38.34 -    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
   38.35 +    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
   38.36        (fn (quant, props) => fn ctxt =>
   38.37          SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
   38.38      "insert subgoal (dynamic instantiation)" #>
   38.39    Method.setup @{binding thin_tac}
   38.40 -    (Args.goal_spec -- Scan.lift Args.name_source >>
   38.41 +    (Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
   38.42        (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
   38.43        "remove premise (dynamic instantiation)");
   38.44  
    39.1 --- a/src/Pure/pure_thy.ML	Wed Jan 22 10:13:40 2014 +0100
    39.2 +++ b/src/Pure/pure_thy.ML	Wed Jan 22 17:14:27 2014 +0100
    39.3 @@ -70,8 +70,9 @@
    39.4          "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
    39.5          "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
    39.6          "float_position", "xnum_position", "index", "struct", "tid_position",
    39.7 -        "tvar_position", "id_position", "longid_position", "var_position", "str_position",
    39.8 -        "cartouche_position", "type_name", "class_name"]))
    39.9 +        "tvar_position", "id_position", "longid_position", "var_position",
   39.10 +        "str_position", "string_position", "cartouche_position", "type_name",
   39.11 +        "class_name"]))
   39.12    #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   39.13    #> Sign.add_syntax_i
   39.14     [("",            typ "prop' => prop",               Delimfix "_"),
   39.15 @@ -155,6 +156,7 @@
   39.16      ("_position",   typ "longid => longid_position",   Delimfix "_"),
   39.17      ("_position",   typ "var => var_position",         Delimfix "_"),
   39.18      ("_position",   typ "str_token => str_position",   Delimfix "_"),
   39.19 +    ("_position",   typ "string_token => string_position", Delimfix "_"),
   39.20      ("_position",   typ "cartouche => cartouche_position", Delimfix "_"),
   39.21      ("_type_constraint_", typ "'a",                    NoSyn),
   39.22      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    40.1 --- a/src/Tools/induct_tacs.ML	Wed Jan 22 10:13:40 2014 +0100
    40.2 +++ b/src/Tools/induct_tacs.ML	Wed Jan 22 17:14:27 2014 +0100
    40.3 @@ -122,13 +122,14 @@
    40.4  val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
    40.5  
    40.6  val varss =
    40.7 -  Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
    40.8 +  Parse.and_list'
    40.9 +    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
   40.10  
   40.11  in
   40.12  
   40.13  val setup =
   40.14    Method.setup @{binding case_tac}
   40.15 -    (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
   40.16 +    (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
   40.17        (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
   40.18      "unstructured case analysis on types" #>
   40.19    Method.setup @{binding induct_tac}
    41.1 --- a/src/ZF/Tools/ind_cases.ML	Wed Jan 22 10:13:40 2014 +0100
    41.2 +++ b/src/ZF/Tools/ind_cases.ML	Wed Jan 22 17:14:27 2014 +0100
    41.3 @@ -57,7 +57,7 @@
    41.4  
    41.5  val setup =
    41.6    Method.setup @{binding "ind_cases"}
    41.7 -    (Scan.lift (Scan.repeat1 Args.name_source) >>
    41.8 +    (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
    41.9        (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
   41.10      "dynamic case analysis on sets";
   41.11  
    42.1 --- a/src/ZF/UNITY/SubstAx.thy	Wed Jan 22 10:13:40 2014 +0100
    42.2 +++ b/src/ZF/UNITY/SubstAx.thy	Wed Jan 22 17:14:27 2014 +0100
    42.3 @@ -375,7 +375,7 @@
    42.4  *}
    42.5  
    42.6  method_setup ensures = {*
    42.7 -    Args.goal_spec -- Scan.lift Args.name_source >>
    42.8 +    Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
    42.9      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
   42.10  *} "for proving progress properties"
   42.11