# HG changeset patch # User wenzelm # Date 1390407267 -3600 # Node ID 0ee5c17f22073459d75477f6f113f63d758c2291 # Parent 761e40ce91bc2bb55ec991df548afe94b4ab79a5# Parent 497693486858c936145a1a95322aa1e5e26bc765 merged diff -r 761e40ce91bc -r 0ee5c17f2207 NEWS --- a/NEWS Wed Jan 22 10:13:40 2014 +0100 +++ b/NEWS Wed Jan 22 17:14:27 2014 +0100 @@ -43,6 +43,10 @@ context discipline. See also Assumption.add_assumes and the more primitive Thm.assume_hyps. +* Inner syntax token language allows regular quoted strings "..." +(only makes sense in practice, if outer syntax is delimited +differently). + *** HOL *** diff -r 761e40ce91bc -r 0ee5c17f2207 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Jan 22 10:13:40 2014 +0100 +++ b/etc/isar-keywords.el Wed Jan 22 17:14:27 2014 +0100 @@ -272,8 +272,10 @@ "syntax" "syntax_declaration" "term" + "term_cartouche" "termination" "text" + "text_cartouche" "text_raw" "then" "theorem" @@ -453,6 +455,7 @@ "solve_direct" "spark_status" "term" + "term_cartouche" "thm" "thm_deps" "thy_deps" @@ -591,6 +594,7 @@ "syntax" "syntax_declaration" "text" + "text_cartouche" "text_raw" "theorems" "translations" diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Jan 22 17:14:27 2014 +0100 @@ -451,12 +451,12 @@ @{command_def "datatype_new"} & : & @{text "local_theory \ local_theory"} \end{matharray} -@{rail " +@{rail \ @@{command datatype_new} target? @{syntax dt_options}? \ (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and') ; @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')' -"} +\} The syntactic entity \synt{target} can be used to specify a local context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference @@ -485,13 +485,13 @@ The left-hand sides of the datatype equations specify the name of the type to define, its type parameters, and additional information: -@{rail " +@{rail \ @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix? ; @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')' ; @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')' -"} +\} \noindent The syntactic entity \synt{name} denotes an identifier, \synt{typefree} @@ -504,10 +504,10 @@ Inside a mutually recursive specification, all defined datatypes must mention exactly the same type variables in the same order. -@{rail " +@{rail \ @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \ @{syntax dt_sel_defaults}? mixfix? -"} +\} \medskip @@ -517,9 +517,9 @@ can be supplied at the front to override the default name (@{text t.is_C\<^sub>j}). -@{rail " +@{rail \ @{syntax_def ctor_arg}: type | '(' name ':' type ')' -"} +\} \medskip @@ -529,9 +529,9 @@ (@{text un_C\<^sub>ji}). The same selector names can be reused for several constructors as long as they share the same type. -@{rail " +@{rail \ @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')' -"} +\} \noindent Given a constructor @@ -552,9 +552,9 @@ @{command_def "datatype_new_compat"} & : & @{text "local_theory \ local_theory"} \end{matharray} -@{rail " +@{rail \ @@{command datatype_new_compat} names -"} +\} \noindent The old datatype package provides some functionality that is not yet replicated @@ -1346,11 +1346,11 @@ @{command_def "primrec_new"} & : & @{text "local_theory \ local_theory"} \end{matharray} -@{rail " +@{rail \ @@{command primrec_new} target? fixes \ @'where' (@{syntax pr_equation} + '|') ; @{syntax_def pr_equation}: thmdecl? prop -"} +\} *} @@ -1568,10 +1568,10 @@ @{command_def "codatatype"} & : & @{text "local_theory \ local_theory"} \end{matharray} -@{rail " +@{rail \ @@{command codatatype} target? \ (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and') -"} +\} \noindent Definitions of codatatypes have almost exactly the same syntax as for datatypes @@ -2235,7 +2235,7 @@ @{command_def "primcorecursive"} & : & @{text "local_theory \ proof(prove)"} \end{matharray} -@{rail " +@{rail \ (@@{command primcorec} | @@{command primcorecursive}) target? \ @{syntax pcr_option}? fixes @'where' (@{syntax pcr_formula} + '|') @@ -2243,7 +2243,7 @@ @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')' ; @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))? -"} +\} The optional target is potentially followed by a corecursion-specific option: @@ -2319,11 +2319,11 @@ @{command_def "bnf"} & : & @{text "local_theory \ proof(prove)"} \end{matharray} -@{rail " +@{rail \ @@{command bnf} target? (name ':')? typ \ 'map:' term ('sets:' (term +))? 'bd:' term \ ('wits:' (term +))? ('rel:' term)? -"} +\} *} @@ -2336,7 +2336,7 @@ @{text "bnf_decl"} & : & @{text "local_theory \ local_theory"} \end{matharray} -@{rail " +@{rail \ @@{command bnf_decl} target? @{syntax dt_name} ; @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix? @@ -2344,7 +2344,7 @@ @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')' ; @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')' -"} +\} Declares a fresh type and fresh constants (map, set, relator, cardinal bound) and asserts the bnf properties for these constants as axioms. Additionally, @@ -2364,9 +2364,9 @@ @{command_def "print_bnfs"} & : & @{text "local_theory \"} \end{matharray} -@{rail " +@{rail \ @@{command print_bnfs} -"} +\} *} @@ -2410,7 +2410,7 @@ @{command_def "wrap_free_constructors"} & : & @{text "local_theory \ proof(prove)"} \end{matharray} -@{rail " +@{rail \ @@{command wrap_free_constructors} target? @{syntax dt_options} \ term_list name @{syntax wfc_discs_sels}? ; @@ -2419,7 +2419,7 @@ @{syntax_def name_term}: (name ':' term) ; X_list: '[' (X + ',') ']' -"} +\} % options: no_discs_sels no_code rep_compat diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarImplementation/Isar.thy --- a/src/Doc/IsarImplementation/Isar.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarImplementation/Isar.thy Wed Jan 22 17:14:27 2014 +0100 @@ -563,9 +563,9 @@ @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ @@{ML_antiquotation attributes} attributes - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarImplementation/Logic.thy Wed Jan 22 17:14:27 2014 +0100 @@ -196,7 +196,7 @@ @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ @@{ML_antiquotation class} nameref ; @@{ML_antiquotation sort} sort @@ -206,7 +206,7 @@ @@{ML_antiquotation nonterminal}) nameref ; @@{ML_antiquotation typ} type - "} + \} \begin{description} @@ -444,7 +444,7 @@ @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ (@@{ML_antiquotation const_name} | @@{ML_antiquotation const_abbrev}) nameref ; @@ -453,7 +453,7 @@ @@{ML_antiquotation term} term ; @@{ML_antiquotation prop} prop - "} + \} \begin{description} @@ -780,7 +780,7 @@ @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ @@{ML_antiquotation ctyp} typ ; @@{ML_antiquotation cterm} term @@ -793,7 +793,7 @@ ; @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \ @'by' method method? - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarImplementation/ML.thy --- a/src/Doc/IsarImplementation/ML.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarImplementation/ML.thy Wed Jan 22 17:14:27 2014 +0100 @@ -666,9 +666,9 @@ concept of \emph{ML antiquotation}. The standard token language of ML is augmented by special syntactic entities of the following form: - @{rail " + @{rail \ @{syntax_def antiquote}: '@{' nameref args '}' - "} + \} Here @{syntax nameref} and @{syntax args} are regular outer syntax categories \cite{isabelle-isar-ref}. Attributes and proof methods @@ -699,9 +699,9 @@ @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ @@{ML_antiquotation make_string} - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarImplementation/Prelim.thy --- a/src/Doc/IsarImplementation/Prelim.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarImplementation/Prelim.thy Wed Jan 22 17:14:27 2014 +0100 @@ -165,11 +165,11 @@ @{ML_antiquotation_def "theory_context"} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ @@{ML_antiquotation theory} nameref? ; @@{ML_antiquotation theory_context} nameref - "} + \} \begin{description} @@ -1025,9 +1025,9 @@ @{ML_antiquotation_def "binding"} & : & @{text ML_antiquotation} \\ \end{matharray} - @{rail " + @{rail \ @@{ML_antiquotation binding} name - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Document_Preparation.thy --- a/src/Doc/IsarRef/Document_Preparation.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Document_Preparation.thy Wed Jan 22 17:14:27 2014 +0100 @@ -47,13 +47,13 @@ markup commands, but have a different status within Isabelle/Isar syntax. - @{rail " + @{rail \ (@@{command chapter} | @@{command section} | @@{command subsection} | @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text} ; (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} | @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text} - "} + \} \begin{description} @@ -148,7 +148,7 @@ context. %% FIXME less monolithic presentation, move to individual sections!? - @{rail " + @{rail \ '@{' antiquotation '}' ; @{syntax_def antiquotation}: @@ -176,7 +176,7 @@ @@{antiquotation ML_op} options @{syntax name} | @@{antiquotation ML_type} options @{syntax name} | @@{antiquotation ML_struct} options @{syntax name} | - @@{antiquotation \"file\"} options @{syntax name} | + @@{antiquotation "file"} options @{syntax name} | @@{antiquotation file_unchecked} options @{syntax name} | @@{antiquotation url} options @{syntax name} ; @@ -187,7 +187,7 @@ styles: '(' (style + ',') ')' ; style: (@{syntax name} +) - "} + \} Note that the syntax of antiquotations may \emph{not} include source comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} nor verbatim @@ -404,11 +404,11 @@ presentation tags, to indicate some modification in the way it is printed in the document. - @{rail " + @{rail \ @{syntax_def tags}: ( tag * ) ; tag: '%' (@{syntax ident} | @{syntax string}) - "} + \} Some tags are pre-declared for certain classes of commands, serving as default markup if no tags are given in the text: @@ -457,7 +457,9 @@ @{antiquotation_def "rail"} & : & @{text antiquotation} \\ \end{matharray} - @{rail "'rail' string"} + @{rail \ + 'rail' (@{syntax string} | @{syntax cartouche}) + \} The @{antiquotation rail} antiquotation allows to include syntax diagrams into Isabelle documents. {\LaTeX} requires the style file @@ -468,7 +470,7 @@ The rail specification language is quoted here as Isabelle @{syntax string}; it has its own grammar given below. - @{rail " + @{rail \ rule? + ';' ; rule: ((identifier | @{syntax antiquotation}) ':')? body @@ -479,13 +481,13 @@ ; atom: '(' body? ')' | identifier | '@'? (string | @{syntax antiquotation}) | - '\\\\\\\\' - "} + '\' + \} The lexical syntax of @{text "identifier"} coincides with that of @{syntax ident} in regular Isabelle syntax, but @{text string} uses single quotes instead of double quotes of the standard @{syntax - string} category, to avoid extra escapes. + string} category. Each @{text rule} defines a formal language (with optional name), using a notation that is similar to EBNF or regular expressions with @@ -496,62 +498,62 @@ \item Empty @{verbatim "()"} - @{rail "()"} + @{rail \()\} \item Nonterminal @{verbatim "A"} - @{rail "A"} + @{rail \A\} \item Nonterminal via Isabelle antiquotation @{verbatim "@{syntax method}"} - @{rail "@{syntax method}"} + @{rail \@{syntax method}\} \item Terminal @{verbatim "'xyz'"} - @{rail "'xyz'"} + @{rail \'xyz'\} \item Terminal in keyword style @{verbatim "@'xyz'"} - @{rail "@'xyz'"} + @{rail \@'xyz'\} \item Terminal via Isabelle antiquotation @{verbatim "@@{method rule}"} - @{rail "@@{method rule}"} + @{rail \@@{method rule}\} \item Concatenation @{verbatim "A B C"} - @{rail "A B C"} + @{rail \A B C\} \item Newline inside concatenation @{verbatim "A B C \ D E F"} - @{rail "A B C \ D E F"} + @{rail \A B C \ D E F\} \item Variants @{verbatim "A | B | C"} - @{rail "A | B | C"} + @{rail \A | B | C\} \item Option @{verbatim "A ?"} - @{rail "A ?"} + @{rail \A ?\} \item Repetition @{verbatim "A *"} - @{rail "A *"} + @{rail \A *\} \item Repetition with separator @{verbatim "A * sep"} - @{rail "A * sep"} + @{rail \A * sep\} \item Strict repetition @{verbatim "A +"} - @{rail "A +"} + @{rail \A +\} \item Strict repetition with separator @{verbatim "A + sep"} - @{rail "A + sep"} + @{rail \A + sep\} \end{itemize} *} @@ -564,10 +566,9 @@ @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \"} \\ \end{matharray} - @{rail " + @{rail \ @@{command display_drafts} (@{syntax name} +) - - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Generic.thy --- a/src/Doc/IsarRef/Generic.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Generic.thy Wed Jan 22 17:14:27 2014 +0100 @@ -34,9 +34,9 @@ @{command_def "print_options"} & : & @{text "context \"} \\ \end{matharray} - @{rail " + @{rail \ @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))? - "} + \} \begin{description} @@ -70,14 +70,14 @@ @{method_def fail} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs} ; (@@{method erule} | @@{method drule} | @@{method frule}) ('(' @{syntax nat} ')')? @{syntax thmrefs} ; (@@{method intro} | @@{method elim}) @{syntax thmrefs}? - "} + \} \begin{description} @@ -136,7 +136,7 @@ @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{attribute tagged} @{syntax name} @{syntax name} ; @@{attribute untagged} @{syntax name} @@ -146,7 +146,7 @@ (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs} ; @@{attribute rotated} @{syntax int}? - "} + \} \begin{description} @@ -201,11 +201,11 @@ @{method_def split} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ @@{method subst} ('(' 'asm' ')')? \ ('(' (@{syntax nat}+) ')')? @{syntax thmref} ; @@{method split} @{syntax thmrefs} - "} + \} These methods provide low-level facilities for equational reasoning that are intended for specialized applications only. Normally, @@ -304,7 +304,7 @@ @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \ ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} ) @@ -319,7 +319,7 @@ ; dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') - "} + \} \begin{description} @@ -406,7 +406,7 @@ @{method_def simp_all} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * ) ; @@ -414,7 +414,7 @@ ; @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs} - "} + \} \begin{description} @@ -608,10 +608,10 @@ @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} - @{rail " + @{rail \ (@@{attribute simp} | @@{attribute split} | @@{attribute cong}) (() | 'add' | 'del') - "} + \} \begin{description} @@ -923,13 +923,13 @@ simproc & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '=' @{syntax text} \ (@'identifier' (@{syntax nameref}+))? ; @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+) - "} + \} \begin{description} @@ -1229,12 +1229,12 @@ @{attribute_def simplified} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{attribute simplified} opt? @{syntax thmrefs}? ; opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')' - "} + \} \begin{description} @@ -1490,13 +1490,13 @@ @{attribute_def swapped} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}? ; @@{attribute rule} 'del' ; @@{attribute iff} (((() | 'add') '?'?) | 'del') - "} + \} \begin{description} @@ -1562,9 +1562,9 @@ @{method_def contradiction} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ @@{method rule} @{syntax thmrefs}? - "} + \} \begin{description} @@ -1603,7 +1603,7 @@ @{method_def deepen} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ @@{method blast} @{syntax nat}? (@{syntax clamod} * ) ; @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * ) @@ -1624,7 +1624,7 @@ ('cong' | 'split') (() | 'add' | 'del') | 'iff' (((() | 'add') '?'?) | 'del') | (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs} - "} + \} \begin{description} @@ -1735,11 +1735,11 @@ @{method_def clarsimp} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ (@@{method safe} | @@{method clarify}) (@{syntax clamod} * ) ; @@{method clarsimp} (@{syntax clasimpmod} * ) - "} + \} \begin{description} @@ -1926,13 +1926,13 @@ Generic tools may refer to the information provided by object-logic declarations internally. - @{rail " + @{rail \ @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}? ; @@{attribute atomize} ('(' 'full' ')')? ; @@{attribute rule_format} ('(' 'noasm' ')')? - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/HOL_Specific.thy Wed Jan 22 17:14:27 2014 +0100 @@ -96,17 +96,17 @@ introduction rule. The default rule declarations of Isabelle/HOL already take care of most common situations. - @{rail " + @{rail \ (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} | @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set}) @{syntax target}? \ - @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \ + @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \ (@'monos' @{syntax thmrefs})? ; clauses: (@{syntax thmdecl}? @{syntax prop} + '|') ; @@{attribute (HOL) mono} (() | 'add' | 'del') - "} + \} \begin{description} @@ -264,11 +264,11 @@ @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} - @{rail " - @@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations + @{rail \ + @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations ; (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts? - @{syntax \"fixes\"} \ @'where' equations + @{syntax "fixes"} \ @'where' equations ; equations: (@{syntax thmdecl}? @{syntax prop} + '|') @@ -278,7 +278,7 @@ @@{command (HOL) termination} @{syntax term}? ; @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and') - "} + \} \begin{description} @@ -508,7 +508,7 @@ @{method_def (HOL) induction_schema} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ @@{method (HOL) relation} @{syntax term} ; @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * ) @@ -518,7 +518,7 @@ @@{method (HOL) induction_schema} ; orders: ( 'max' | 'min' | 'ms' ) * - "} + \} \begin{description} @@ -574,11 +574,11 @@ @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{command (HOL) partial_function} @{syntax target}? - '(' @{syntax nameref} ')' @{syntax \"fixes\"} \ + '(' @{syntax nameref} ')' @{syntax "fixes"} \ @'where' @{syntax thmdecl}? @{syntax prop} - "} + \} \begin{description} @@ -649,7 +649,7 @@ "recdef_tc"} for defining recursive are mostly obsolete; @{command (HOL) "function"} or @{command (HOL) "fun"} should be used instead. - @{rail " + @{rail \ @@{command (HOL) recdef} ('(' @'permissive' ')')? \ @{syntax name} @{syntax term} (@{syntax prop} +) hints? ; @@ -661,7 +661,7 @@ (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod} ; tc: @{syntax nameref} ('(' @{syntax nat} ')')? - "} + \} \begin{description} @@ -695,10 +695,10 @@ @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} | @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del') - "} + \} *} @@ -710,7 +710,7 @@ @{command_def (HOL) "rep_datatype"} & : & @{text "theory \ proof(prove)"} \\ \end{matharray} - @{rail " + @{rail \ @@{command (HOL) datatype} (spec + @'and') ; @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) @@ -719,7 +719,7 @@ spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|') ; cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}? - "} + \} \begin{description} @@ -873,12 +873,12 @@ @{command_def (HOL) "record"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ @@{command (HOL) record} @{syntax typespec_sorts} '=' \ (@{syntax type} '+')? (constdecl +) ; constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}? - "} + \} \begin{description} @@ -1074,14 +1074,13 @@ type_synonym} from Isabelle/Pure merely introduces syntactic abbreviations, without any logical significance. - @{rail " + @{rail \ @@{command (HOL) typedef} abs_type '=' rep_set ; - abs_type: @{syntax typespec_sorts} @{syntax mixfix}? ; rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})? - "} + \} \begin{description} @@ -1198,10 +1197,9 @@ @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \ proof(prove)"} \end{matharray} - @{rail " + @{rail \ @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term} - ; - "} + \} \begin{description} @@ -1265,28 +1263,26 @@ packages. The user should consider using these two new packages for lifting definitions and transporting theorems. - @{rail " - @@{command (HOL) quotient_type} (spec); - + @{rail \ + @@{command (HOL) quotient_type} (spec) + ; spec: @{syntax typespec} @{syntax mixfix}? '=' \ @{syntax type} '/' ('partial' ':')? @{syntax term} \ - (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?; - "} - - @{rail " + (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})? + \} + + @{rail \ @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \ - @{syntax term} 'is' @{syntax term}; - + @{syntax term} 'is' @{syntax term} + ; constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? - "} - - @{rail " + \} + + @{rail \ @@{method (HOL) lifting} @{syntax thmrefs}? ; - @@{method (HOL) lifting_setup} @{syntax thmrefs}? - ; - "} + \} \begin{description} @@ -1399,12 +1395,12 @@ @{command_def (HOL) "ax_specification"} & : & @{text "theory \ proof(prove)"} \\ \end{matharray} - @{rail " - (@@{command (HOL) specification} | @@{command (HOL) ax_specification}) - '(' (decl +) ')' \ (@{syntax thmdecl}? @{syntax prop} +) - ; - decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?) - "} + @{rail \ + (@@{command (HOL) specification} | @@{command (HOL) ax_specification}) + '(' (decl +) ')' \ (@{syntax thmdecl}? @{syntax prop} +) + ; + decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?) + \} \begin{description} @@ -1458,10 +1454,10 @@ @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and @{file "~~/src/HOL/Library/Monad_Syntax.thy"}. - @{rail " + @{rail \ (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) - (@{syntax nameref} (@{syntax term} + ) + @'and') - "} + (@{syntax nameref} (@{syntax term} + ) + @'and') + \} \begin{description} @@ -1490,9 +1486,9 @@ @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{attribute (HOL) split_format} ('(' 'complete' ')')? - "} + \} \begin{description} @@ -1626,27 +1622,27 @@ @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \ @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?; - "} - - @{rail " + \} + + @{rail \ @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \ 'is' @{syntax term} (@'parametric' @{syntax thmref})?; - "} - - @{rail " + \} + + @{rail \ @@{command (HOL) lifting_forget} @{syntax nameref}; - "} - - @{rail " + \} + + @{rail \ @@{command (HOL) lifting_update} @{syntax nameref}; - "} - - @{rail " + \} + + @{rail \ @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?; - "} + \} \begin{description} @@ -1828,14 +1824,11 @@ them as necessary when parsing a term. See \cite{traytel-berghofer-nipkow-2011} for details. - @{rail " + @{rail \ @@{attribute (HOL) coercion} (@{syntax term})? ; - "} - @{rail " @@{attribute (HOL) coercion_map} (@{syntax term})? - ; - "} + \} \begin{description} @@ -1902,9 +1895,9 @@ @{method_def (HOL) iprover} & : & @{text method} \\ \end{matharray} - @{rail " - @@{method (HOL) iprover} ( @{syntax rulemod} * ) - "} + @{rail \ + @@{method (HOL) iprover} (@{syntax rulemod} *) + \} \begin{description} @@ -1934,14 +1927,13 @@ @{method_def (HOL) "metis"} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ @@{method (HOL) meson} @{syntax thmrefs}? ; - @@{method (HOL) metis} ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')? @{syntax thmrefs}? - "} + \} \begin{description} @@ -1968,13 +1960,13 @@ @{attribute_def (HOL) algebra} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{method (HOL) algebra} ('add' ':' @{syntax thmrefs})? ('del' ':' @{syntax thmrefs})? ; @@{attribute (HOL) algebra} (() | 'add' | 'del') - "} + \} \begin{description} @@ -2051,9 +2043,9 @@ @{method_def (HOL) "coherent"} & : & @{text method} \\ \end{matharray} - @{rail " + @{rail \ @@{method (HOL) coherent} @{syntax thmrefs}? - "} + \} \begin{description} @@ -2081,7 +2073,7 @@ @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \ theory"} \end{matharray} - @{rail " + @{rail \ @@{command (HOL) try} ; @@ -2094,13 +2086,10 @@ @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? ) ; - args: ( @{syntax name} '=' value + ',' ) ; - facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')' - ; - "} % FIXME check args "value" + \} % FIXME check args "value" \begin{description} @@ -2150,7 +2139,7 @@ @{command_def (HOL) "find_unused_assms"} & : & @{text "context \"} \end{matharray} - @{rail " + @{rail \ @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term} ; @@ -2171,13 +2160,10 @@ @@{command (HOL) find_unused_assms} @{syntax name}? ; - modes: '(' (@{syntax name} +) ')' ; - args: ( @{syntax name} '=' value + ',' ) - ; - "} % FIXME check "value" + \} % FIXME check "value" \begin{description} @@ -2320,7 +2306,7 @@ @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} - @{rail " + @{rail \ @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule? ; @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule? @@ -2329,9 +2315,8 @@ ; @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and') ; - rule: 'rule' ':' @{syntax thmref} - "} + \} \begin{description} @@ -2413,7 +2398,7 @@ @{command_def (HOL) "code_pred"} & : & @{text "theory \ proof(prove)"} \end{matharray} - @{rail " + @{rail \ @@{command (HOL) export_code} ( constexpr + ) \ ( ( @'in' target ( @'module_name' @{syntax string} ) ? \ ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ? @@ -2553,7 +2538,7 @@ ; modes: mode @'as' const - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Inner_Syntax.thy --- a/src/Doc/IsarRef/Inner_Syntax.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Wed Jan 22 17:14:27 2014 +0100 @@ -46,7 +46,7 @@ These diagnostic commands assist interactive development by printing internal logical entities in a human-readable fashion. - @{rail " + @{rail \ @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})? ; @@{command term} @{syntax modes}? @{syntax term} @@ -59,9 +59,8 @@ ; @@{command print_state} @{syntax modes}? ; - @{syntax_def modes}: '(' (@{syntax name} + ) ')' - "} + \} \begin{description} @@ -358,7 +357,7 @@ to specify any context-free priority grammar, which is more general than the fixity declarations of ML and Prolog. - @{rail " + @{rail \ @{syntax_def mixfix}: '(' @{syntax template} prios? @{syntax nat}? | (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} | @@ -369,7 +368,7 @@ template: string ; prios: '[' (@{syntax nat} + ',') ']' - "} + \} The string given as @{text template} may include literal text, spacing, blocks, and arguments (denoted by ``@{text _}''); the @@ -559,7 +558,7 @@ allows to add or delete mixfix annotations for of existing logical entities within the current context. - @{rail " + @{rail \ (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}? @{syntax mode}? \ (@{syntax nameref} @{syntax mixfix} + @'and') ; @@ -567,7 +566,7 @@ (@{syntax nameref} @{syntax mixfix} + @'and') ; @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and') - "} + \} \begin{description} @@ -631,18 +630,19 @@ @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\ @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ - @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\"} @{verbatim "''"} \\ + @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\"} @{verbatim "\""} \\ @{syntax_def (inner) cartouche} & = & @{verbatim "\"} @{text "\"} @{verbatim "\"} \\ \end{supertabular} \end{center} The token categories @{syntax (inner) num_token}, @{syntax (inner) float_token}, @{syntax (inner) xnum_token}, @{syntax (inner) - str_token}, and @{syntax (inner) cartouche} are not used in Pure. - Object-logics may implement numerals and string literals by adding - appropriate syntax declarations, together with some translation - functions (e.g.\ see Isabelle/HOL). + str_token}, @{syntax (inner) string_token}, and @{syntax (inner) + cartouche} are not used in Pure. Object-logics may implement + numerals and string literals by adding appropriate syntax + declarations, together with some translation functions (e.g.\ see + @{file "~~/src/HOL/Tools/string_syntax.ML"}). The derived categories @{syntax_def (inner) num_const}, @{syntax_def (inner) float_const}, and @{syntax_def (inner) num_const} provide @@ -1216,7 +1216,7 @@ @{command translations}) are required to turn resulting parse trees into proper representations of formal entities again. - @{rail " + @{rail \ @@{command nonterminal} (@{syntax name} + @'and') ; (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +) @@ -1230,7 +1230,7 @@ mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')') ; transpat: ('(' @{syntax nameref} ')')? @{syntax string} - "} + \} \begin{description} @@ -1463,7 +1463,7 @@ manipulations of inner syntax, at the expense of some complexity and obscurity in the implementation. - @{rail " + @{rail \ ( @@{command parse_ast_translation} | @@{command parse_translation} | @@{command print_translation} | @@{command typed_print_translation} | @@{command print_ast_translation}) @{syntax text} @@ -1472,7 +1472,7 @@ @@{ML_antiquotation type_syntax} | @@{ML_antiquotation const_syntax} | @@{ML_antiquotation syntax_const}) name - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Misc.thy --- a/src/Doc/IsarRef/Misc.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Misc.thy Wed Jan 22 17:14:27 2014 +0100 @@ -20,7 +20,7 @@ @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} - @{rail " + @{rail \ (@@{command print_theory} | @@{command print_theorems}) ('!'?) ; @@ -37,7 +37,7 @@ @@{command thm_deps} @{syntax thmrefs} ; @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))? - "} + \} These commands print certain parts of the theory and proof context. Note that there are some further ones available, such as for the set @@ -121,9 +121,9 @@ @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \"} \\ \end{matharray} - @{rail " + @{rail \ (@@{command cd} | @@{command use_thy}) @{syntax name} - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Outer_Syntax.thy --- a/src/Doc/IsarRef/Outer_Syntax.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Outer_Syntax.thy Wed Jan 22 17:14:27 2014 +0100 @@ -72,9 +72,9 @@ @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \"} \\ \end{matharray} - @{rail " + @{rail \ @@{command help} (@{syntax name} * ) - "} + \} \begin{description} @@ -233,14 +233,14 @@ Already existing objects are usually referenced by @{syntax nameref}. - @{rail " + @{rail \ @{syntax_def name}: @{syntax ident} | @{syntax symident} | @{syntax string} | @{syntax nat} ; @{syntax_def parname}: '(' @{syntax name} ')' ; @{syntax_def nameref}: @{syntax name} | @{syntax longident} - "} + \} *} @@ -250,11 +250,11 @@ natural numbers and floating point numbers. These are combined as @{syntax int} and @{syntax real} as follows. - @{rail " + @{rail \ @{syntax_def int}: @{syntax nat} | '-' @{syntax nat} ; @{syntax_def real}: @{syntax float} | @{syntax int} - "} + \} Note that there is an overlap with the category @{syntax name}, which also includes @{syntax nat}. @@ -271,11 +271,11 @@ @{verbatim "--"}~@{syntax text}. Any number of these may occur within Isabelle/Isar commands. - @{rail " + @{rail \ @{syntax_def text}: @{syntax verbatim} | @{syntax nameref} ; @{syntax_def comment}: '--' @{syntax text} - "} + \} *} @@ -288,13 +288,13 @@ intersection of these classes. The syntax of type arities is given directly at the outer level. - @{rail " + @{rail \ @{syntax_def classdecl}: @{syntax name} (('<' | '\') (@{syntax nameref} + ','))? ; @{syntax_def sort}: @{syntax nameref} ; @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort} - "} + \} *} @@ -314,38 +314,38 @@ by commands or other keywords already (such as @{verbatim "="} or @{verbatim "+"}). - @{rail " + @{rail \ @{syntax_def type}: @{syntax nameref} | @{syntax typefree} | @{syntax typevar} ; @{syntax_def term}: @{syntax nameref} | @{syntax var} ; @{syntax_def prop}: @{syntax term} - "} + \} Positional instantiations are indicated by giving a sequence of terms, or the placeholder ``@{text _}'' (underscore), which means to skip a position. - @{rail " + @{rail \ @{syntax_def inst}: '_' | @{syntax term} ; @{syntax_def insts}: (@{syntax inst} *) - "} + \} Type declarations and definitions usually refer to @{syntax typespec} on the left-hand side. This models basic type constructor application at the outer syntax level. Note that only plain postfix notation is available here, but no infixes. - @{rail " + @{rail \ @{syntax_def typespec}: (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name} ; @{syntax_def typespec_sorts}: (() | (@{syntax typefree} ('::' @{syntax sort})?) | '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name} - "} + \} *} @@ -356,11 +356,11 @@ specified via patterns of the form ``@{text "(\ p\<^sub>1 \ p\<^sub>n)"}''. This works both for @{syntax term} and @{syntax prop}. - @{rail " + @{rail \ @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')' ; @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')' - "} + \} \medskip Declarations of local variables @{text "x :: \"} and logical propositions @{text "a : \"} represent different views on @@ -370,11 +370,11 @@ references of current facts). In any case, Isar proof elements usually admit to introduce multiple such items simultaneously. - @{rail " + @{rail \ @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})? ; @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +) - "} + \} The treatment of multiple declarations corresponds to the complementary focus of @{syntax vars} versus @{syntax props}. In @@ -398,7 +398,7 @@ any atomic entity, including any @{syntax keyword} conforming to @{syntax symident}. - @{rail " + @{rail \ @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} | @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} | @{syntax keyword} | @{syntax cartouche} @@ -408,7 +408,7 @@ @{syntax_def args}: arg * ; @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']' - "} + \} Theorem specifications come in several flavors: @{syntax axmdecl} and @{syntax thmdecl} usually refer to axioms, assumptions or @@ -443,7 +443,7 @@ This form of in-place declarations is particularly useful with commands like @{command "declare"} and @{command "using"}. - @{rail " + @{rail \ @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':' ; @{syntax_def thmdecl}: thmbind ':' @@ -460,7 +460,7 @@ thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes} ; selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')' - "} + \} *} end diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Proof.thy --- a/src/Doc/IsarRef/Proof.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Proof.thy Wed Jan 22 17:14:27 2014 +0100 @@ -53,11 +53,11 @@ @{command_def "notepad"} & : & @{text "local_theory \ proof(state)"} \\ \end{matharray} - @{rail " + @{rail \ @@{command notepad} @'begin' ; @@{command end} - "} + \} \begin{description} @@ -183,7 +183,7 @@ exporting some result @{text "x \ t \ \[x]"} yields @{text "\ \[t]"}. - @{rail " + @{rail \ @@{command fix} (@{syntax vars} + @'and') ; (@@{command assume} | @@{command presume}) (@{syntax props} + @'and') @@ -192,7 +192,7 @@ ; def: @{syntax thmdecl}? \ @{syntax name} ('==' | '\') @{syntax term} @{syntax term_pat}? - "} + \} \begin{description} @@ -262,9 +262,9 @@ input process just after type checking. Also note that @{command "def"} does not support polymorphism. - @{rail " + @{rail \ @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and') - "} + \} The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or @{syntax prop_pat} (see \secref{sec:term-decls}). @@ -318,12 +318,12 @@ to the most recently established facts, but only \emph{before} issuing a follow-up claim. - @{rail " + @{rail \ @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and') ; (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding}) (@{syntax thmrefs} + @'and') - "} + \} \begin{description} @@ -429,7 +429,7 @@ contexts of (essentially a big disjunction of eliminated parameters and assumptions, cf.\ \secref{sec:obtain}). - @{rail " + @{rail \ (@@{command lemma} | @@{command theorem} | @@{command corollary} | @@{command schematic_lemma} | @@{command schematic_theorem} | @@{command schematic_corollary}) @{syntax target}? (goal | longgoal) @@ -441,12 +441,12 @@ goal: (@{syntax props} + @'and') ; - longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion + longgoal: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} * ) conclusion ; conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|') ; case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and') - "} + \} \begin{description} @@ -541,12 +541,12 @@ nameref}~@{syntax args} specifications. Note that parentheses may be dropped for single method specifications (with no arguments). - @{rail " + @{rail \ @{syntax_def method}: (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']') ; methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|') - "} + \} Proper Isar proof methods do \emph{not} admit arbitrary goal addressing, but refer either to the first sub-goal or all sub-goals @@ -564,10 +564,10 @@ all goals, and ``@{text "[n-]"}'' to all goals starting from @{text "n"}. - @{rail " + @{rail \ @{syntax_def goal_spec}: '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']' - "} + \} *} @@ -621,15 +621,15 @@ default terminal method. Any remaining goals are always solved by assumption in the very last step. - @{rail " + @{rail \ @@{command proof} method? ; @@{command qed} method? ; - @@{command \"by\"} method method? + @@{command "by"} method method? ; - (@@{command \".\"} | @@{command \"..\"} | @@{command sorry}) - "} + (@@{command "."} | @@{command ".."} | @@{command sorry}) + \} \begin{description} @@ -706,7 +706,7 @@ @{attribute_def "where"} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{method fact} @{syntax thmrefs}? ; @@{method (Pure) rule} @{syntax thmrefs}? @@ -723,10 +723,10 @@ ; @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? ; - @@{attribute \"where\"} + @@{attribute "where"} ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '=' (@{syntax type} | @{syntax term}) * @'and') - "} + \} \begin{description} @@ -846,13 +846,13 @@ @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ \end{matharray} - @{rail " + @{rail \ ( @@{command apply} | @@{command apply_end} ) @{syntax method} ; @@{command defer} @{syntax nat}? ; @@{command prefer} @{syntax nat} - "} + \} \begin{description} @@ -907,10 +907,9 @@ @{command_def "method_setup"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}? - ; - "} + \} \begin{description} @@ -963,12 +962,12 @@ later, provided that the corresponding parameters do \emph{not} occur in the conclusion. - @{rail " + @{rail \ @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and') ; @@{command guess} (@{syntax vars} + @'and') - "} + \} The derived Isar command @{command "obtain"} is defined as follows (where @{text "b\<^sub>1, \, b\<^sub>k"} shall refer to (optional) @@ -1078,11 +1077,11 @@ @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\ \end{matharray} - @{rail " + @{rail \ (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')? ; @@{attribute trans} (() | 'add' | 'del') - "} + \} \begin{description} @@ -1195,7 +1194,7 @@ derived manually become ready to use in advanced case analysis later. - @{rail " + @{rail \ @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')') ; caseref: nameref attributes? @@ -1208,7 +1207,7 @@ @@{attribute params} ((@{syntax name} * ) + @'and') ; @@{attribute consumes} @{syntax int}? - "} + \} \begin{description} @@ -1303,7 +1302,7 @@ the names of the facts in the local context invoked by the @{command "case"} command. - @{rail " + @{rail \ @@{method cases} ('(' 'no_simp' ')')? \ (@{syntax insts} * @'and') rule? ; @@ -1322,7 +1321,7 @@ arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +) ; taking: 'taking' ':' @{syntax insts} - "} + \} \begin{description} @@ -1499,7 +1498,7 @@ @{attribute_def coinduct} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{attribute cases} spec ; @@{attribute induct} spec @@ -1508,7 +1507,7 @@ ; spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del' - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/IsarRef/Spec.thy --- a/src/Doc/IsarRef/Spec.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/IsarRef/Spec.thy Wed Jan 22 17:14:27 2014 +0100 @@ -50,7 +50,7 @@ although some user-interfaces might pretend that trailing input is admissible. - @{rail " + @{rail \ @@{command theory} @{syntax name} imports keywords? \ @'begin' ; imports: @'imports' (@{syntax name} +) @@ -59,7 +59,7 @@ ; keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})? - "} + \} \begin{description} @@ -121,13 +121,13 @@ targets, like @{command "locale"}, @{command "class"}, @{command "instantiation"}, @{command "overloading"}. - @{rail " + @{rail \ @@{command context} @{syntax nameref} @'begin' ; - @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin' + @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin' ; @{syntax_def target}: '(' @'in' @{syntax nameref} ')' - "} + \} \begin{description} @@ -210,14 +210,14 @@ without logical dependencies, which is in contrast to locales and locale interpretation (\secref{sec:locale}). - @{rail " + @{rail \ @@{command bundle} @{syntax target}? \ @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))? ; (@@{command include} | @@{command including}) (@{syntax nameref}+) ; - @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+) - "} + @{syntax_def "includes"}: @'includes' (@{syntax nameref}+) + \} \begin{description} @@ -274,8 +274,8 @@ "defs"} (see \secref{sec:consts}), and raw axioms. In particular, type-inference covers the whole specification as usual. - @{rail " - @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)? + @{rail \ + @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)? ; @@{command definition} @{syntax target}? \ (decl @'where')? @{syntax thmdecl}? @{syntax prop} @@ -284,13 +284,13 @@ (decl @'where')? @{syntax prop} ; - @{syntax_def \"fixes\"}: ((@{syntax name} ('::' @{syntax type})? + @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and') ; specs: (@{syntax thmdecl}? @{syntax props} + @'and') ; decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? - "} + \} \begin{description} @@ -364,12 +364,12 @@ case: it consists of a theorem which is applied to the context by means of an attribute. - @{rail " + @{rail \ (@@{command declaration} | @@{command syntax_declaration}) ('(' @'pervasive' ')')? \ @{syntax target}? @{syntax text} ; @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and') - "} + \} \begin{description} @@ -431,8 +431,8 @@ elements from the locale instances. Redundant locale instances are omitted according to roundup. - @{rail " - @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))? + @{rail \ + @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax "fixes"} + @'and'))? ; instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts) ; @@ -441,7 +441,7 @@ pos_insts: ('_' | @{syntax term})* ; named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and') - "} + \} A locale instance consists of a reference to a locale and either positional or named parameter instantiations. Identical @@ -483,7 +483,7 @@ \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} \indexisarelem{defines}\indexisarelem{notes} - @{rail " + @{rail \ @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? ; @@{command print_locale} '!'? @{syntax nameref} @@ -492,12 +492,12 @@ @{syntax locale_expr} ('+' (@{syntax context_elem}+))? ; @{syntax_def context_elem}: - @'fixes' (@{syntax \"fixes\"} + @'and') | + @'fixes' (@{syntax "fixes"} + @'and') | @'constrains' (@{syntax name} '::' @{syntax type} + @'and') | @'assumes' (@{syntax props} + @'and') | @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') | @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and') - "} + \} \begin{description} @@ -630,7 +630,7 @@ "interpretation"}) and also within proof bodies (@{command "interpret"}). - @{rail " + @{rail \ @@{command interpretation} @{syntax locale_expr} equations? ; @@{command interpret} @{syntax locale_expr} equations? @@ -644,7 +644,7 @@ ; equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') - "} + \} \begin{description} @@ -796,7 +796,7 @@ (notably type-inference). See \cite{isabelle-classes} for a short tutorial. - @{rail " + @{rail \ @@{command class} class_spec @'begin'? ; class_spec: @{syntax name} '=' @@ -809,7 +809,7 @@ @{syntax nameref} ('<' | '\') @{syntax nameref} ) ; @@{command subclass} @{syntax target}? @{syntax nameref} - "} + \} \begin{description} @@ -968,11 +968,11 @@ The @{command "overloading"} target provides a convenient view for end-users. - @{rail " + @{rail \ @@{command overloading} ( spec + ) @'begin' ; spec: @{syntax name} ( '==' | '\' ) @{syntax term} ( '(' @'unchecked' ')' )? - "} + \} \begin{description} @@ -1010,14 +1010,14 @@ @{command_def "attribute_setup"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ @@{command ML_file} @{syntax name} ; (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} ; @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? - "} + \} \begin{description} @@ -1094,13 +1094,13 @@ @{command_def "default_sort"} & : & @{text "local_theory \ local_theory"} \end{matharray} - @{rail " + @{rail \ @@{command classes} (@{syntax classdecl} +) ; @@{command classrel} (@{syntax nameref} ('<' | '\') @{syntax nameref} + @'and') ; @@{command default_sort} @{syntax sort} - "} + \} \begin{description} @@ -1141,13 +1141,13 @@ @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} - @{rail " + @{rail \ @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?) ; @@{command typedecl} @{syntax typespec} @{syntax mixfix}? ; @@{command arities} (@{syntax nameref} '::' @{syntax arity} +) - "} + \} \begin{description} @@ -1219,13 +1219,13 @@ corresponding occurrences on some right-hand side need to be an instance of this, general @{text "d :: \ \ \"} will be disallowed. - @{rail " + @{rail \ @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +) ; @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +) ; opt: '(' @'unchecked'? @'overloaded'? ')' - "} + \} \begin{description} @@ -1259,11 +1259,11 @@ @{command_def "theorems"} & : & @{text "local_theory \ local_theory"} \\ \end{matharray} - @{rail " + @{rail \ (@@{command lemmas} | @@{command theorems}) @{syntax target}? \ (@{syntax thmdef}? @{syntax thmrefs} + @'and') (@'for' (@{syntax vars} + @'and'))? - "} + \} \begin{description} @@ -1302,9 +1302,9 @@ asserted, and records within the internal derivation object how presumed theorems depend on unproven suppositions. - @{rail " + @{rail \ @@{command oracle} @{syntax name} '=' @{syntax text} - "} + \} \begin{description} @@ -1333,10 +1333,10 @@ @{command_def "hide_fact"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ ( @{command hide_class} | @{command hide_type} | @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + ) - "} + \} Isabelle organizes any kind of name declarations (of types, constants, theorems etc.) by separate hierarchically structured name diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/ProgProve/LaTeXsugar.thy --- a/src/Doc/ProgProve/LaTeXsugar.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/ProgProve/LaTeXsugar.thy Wed Jan 22 17:14:27 2014 +0100 @@ -52,7 +52,7 @@ end in Thy_Output.antiquotation @{binding "const_typ"} - (Scan.lift Args.name_source) + (Scan.lift Args.name_inner_syntax) (fn {source = src, context = ctxt, ...} => fn arg => Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty ctxt src [arg])) diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/System/Sessions.thy Wed Jan 22 17:14:27 2014 +0100 @@ -48,7 +48,7 @@ mode @{verbatim "isabelle-root"} for session ROOT files, which is enabled by default for any file of that name. - @{rail " + @{rail \ @{syntax_def session_chapter}: @'chapter' @{syntax name} ; @@ -73,7 +73,7 @@ theories: @'theories' opts? ( @{syntax name} * ) ; files: @'files' ( @{syntax name} + ) - "} + \} \begin{description} diff -r 761e40ce91bc -r 0ee5c17f2207 src/Doc/ZF/ZF_Isar.thy --- a/src/Doc/ZF/ZF_Isar.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Doc/ZF/ZF_Isar.thy Wed Jan 22 17:14:27 2014 +0100 @@ -24,9 +24,9 @@ @{attribute_def (ZF) TC} & : & @{text attribute} \\ \end{matharray} - @{rail " + @{rail \ @@{attribute (ZF) TC} (() | 'add' | 'del') - "} + \} \begin{description} @@ -59,7 +59,7 @@ @{command_def (ZF) "codatatype"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints ; @@ -67,22 +67,22 @@ ; intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +) ; - hints: @{syntax (ZF) \"monos\"}? condefs? \ + hints: @{syntax (ZF) "monos"}? condefs? \ @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? ; - @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs} + @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs} ; condefs: @'con_defs' @{syntax thmrefs} ; @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs} ; @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs} - "} + \} In the following syntax specification @{text "monos"}, @{text typeintros}, and @{text typeelims} are the same as above. - @{rail " + @{rail \ (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints ; @@ -92,8 +92,8 @@ ; con: @{syntax name} ('(' (@{syntax term} ',' +) ')')? ; - hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? - "} + hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? + \} See \cite{isabelle-ZF} for further information on inductive definitions in ZF, but note that this covers the old-style theory @@ -108,9 +108,9 @@ @{command_def (ZF) "primrec"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +) - "} + \} *} @@ -127,14 +127,13 @@ @{command_def (ZF) "inductive_cases"} & : & @{text "theory \ theory"} \\ \end{matharray} - @{rail " + @{rail \ (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name} ; @@{method (ZF) ind_cases} (@{syntax prop} +) ; @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and') - ; - "} + \} *} end diff -r 761e40ce91bc -r 0ee5c17f2207 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/FOL/FOL.thy Wed Jan 22 17:14:27 2014 +0100 @@ -72,7 +72,7 @@ *} method_setup case_tac = {* - Args.goal_spec -- Scan.lift Args.name_source >> + Args.goal_spec -- Scan.lift Args.name_inner_syntax >> (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s)) *} "case_tac emulation (dynamic instantiation!)" diff -r 761e40ce91bc -r 0ee5c17f2207 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 17:14:27 2014 +0100 @@ -106,7 +106,7 @@ end in Thy_Output.antiquotation @{binding "const_typ"} - (Scan.lift Args.name_source) + (Scan.lift Args.name_inner_syntax) (fn {source = src, context = ctxt, ...} => fn arg => Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty ctxt src [arg])) diff -r 761e40ce91bc -r 0ee5c17f2207 src/HOL/SPARK/Tools/fdl_lexer.ML --- a/src/HOL/SPARK/Tools/fdl_lexer.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Wed Jan 22 17:14:27 2014 +0100 @@ -205,7 +205,7 @@ val any_line = whitespace' |-- any_line' --| newline >> (implode o map symbol); -fun gen_comment a b = $$$ a |-- !!! "missing end of comment" +fun gen_comment a b = $$$ a |-- !!! "unclosed comment" (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment; val c_comment = gen_comment "/*" "*/"; diff -r 761e40ce91bc -r 0ee5c17f2207 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/Tools/inductive.ML Wed Jan 22 17:14:27 2014 +0100 @@ -591,7 +591,7 @@ val ind_cases_setup = Method.setup @{binding ind_cases} - (Scan.lift (Scan.repeat1 Args.name_source -- + (Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >> (fn (raw_props, fixes) => fn ctxt => let diff -r 761e40ce91bc -r 0ee5c17f2207 src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/Tools/string_syntax.ML Wed Jan 22 17:14:27 2014 +0100 @@ -38,24 +38,24 @@ val specials = raw_explode "\\\"`'"; fun dest_chr c1 c2 = - let val c = chr (dest_nib c1 * 16 + dest_nib c2) in - if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c - then c - else if c = "\n" then "\" + let val s = chr (dest_nib c1 * 16 + dest_nib c2) in + if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s + then s + else if s = "\n" then "\" else raise Match end; fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2 | dest_char _ = raise Match; -fun syntax_string cs = +fun syntax_string ss = Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, - Ast.Variable (Lexicon.implode_str cs)]; + Ast.Variable (Lexicon.implode_str ss)]; fun char_ast_tr [Ast.Variable str] = - (case Lexicon.explode_str str of - [c] => mk_char c + (case Lexicon.explode_str (str, Position.none) of + [(s, _)] => mk_char s | _ => error ("Single character expected: " ^ str)) | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] = Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2] @@ -69,16 +69,16 @@ (* string *) fun mk_string [] = Ast.Constant @{const_syntax Nil} - | mk_string (c :: cs) = - Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs]; + | mk_string (s :: ss) = + Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss]; fun string_ast_tr [Ast.Variable str] = - (case Lexicon.explode_str str of + (case Lexicon.explode_str (str, Position.none) of [] => Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}] - | cs => mk_string cs) + | ss => mk_string (map Symbol_Pos.symbol ss)) | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] = Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2] | string_ast_tr asts = raise Ast.AST ("string_tr", asts); diff -r 761e40ce91bc -r 0ee5c17f2207 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/UNITY/UNITY_Main.thy Wed Jan 22 17:14:27 2014 +0100 @@ -16,7 +16,7 @@ "for proving safety properties" method_setup ensures_tac = {* - Args.goal_spec -- Scan.lift Args.name_source >> + Args.goal_spec -- Scan.lift Args.name_inner_syntax >> (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) *} "for proving progress properties" diff -r 761e40ce91bc -r 0ee5c17f2207 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Wed Jan 22 17:14:27 2014 +0100 @@ -2,10 +2,12 @@ theory Cartouche_Examples imports Main -keywords "cartouche" :: diag +keywords + "cartouche" "term_cartouche" :: diag and + "text_cartouche" :: thy_decl begin -subsection {* Outer syntax *} +subsection {* Outer syntax: cartouche within command syntax *} ML {* Outer_Syntax.improper_command @{command_spec "cartouche"} "" @@ -17,12 +19,10 @@ cartouche \abc \\\\\ xzy\ -subsection {* Inner syntax *} +subsection {* Inner syntax: string literals via cartouche *} -syntax "_string_cartouche" :: "cartouche_position \ string" ("STR _") - -parse_translation {* - let +ML {* + local val mk_nib = Syntax.const o Lexicon.mark_const o fst o Term.dest_Const o HOLogic.mk_nibble; @@ -39,27 +39,139 @@ | mk_string (s :: ss) = Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss; - fun string_tr ctxt args = - let fun err () = raise TERM ("string_tr", []) in + in + fun string_tr content args = + let fun err () = raise TERM ("string_tr", args) in (case args of [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => (case Term_Position.decode_position p of - SOME (pos, _) => - c $ mk_string (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))) $ p + SOME (pos, _) => c $ mk_string (content (s, pos)) $ p | NONE => err ()) | _ => err ()) end; - in - [(@{syntax_const "_string_cartouche"}, string_tr)] - end + end; +*} + +syntax "_STR_cartouche" :: "cartouche_position \ string" ("STR _") + +parse_translation {* + [(@{syntax_const "_STR_cartouche"}, + K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] *} term "STR \\" term "STR \abc\" -lemma "STR \abc\ @ STR \xyz\ = STR \abcxyz\" by simp +term "STR \abc\ @ STR \xyz\" +term "STR \\\" +term "STR \\001\010\100\" + + +subsection {* Alternate outer and inner syntax: string literals *} + +subsubsection {* Nested quotes *} + +syntax "_STR_string" :: "string_position \ string" ("STR _") + +parse_translation {* + [(@{syntax_const "_STR_string"}, K (string_tr Lexicon.explode_string))] +*} + +term "STR \"\"" +term "STR \"abc\"" +term "STR \"abc\" @ STR \"xyz\"" +term "STR \"\\"" +term "STR \"\001\010\100\"" + + +subsubsection {* Term cartouche and regular quotes *} + +ML {* + Outer_Syntax.improper_command @{command_spec "term_cartouche"} "" + (Parse.inner_syntax Parse.cartouche >> (fn s => + Toplevel.keep (fn state => + let + val ctxt = Toplevel.context_of state; + val t = Syntax.read_term ctxt s; + in writeln (Syntax.string_of_term ctxt t) end))) +*} + +term_cartouche \STR ""\ +term_cartouche \STR "abc"\ +term_cartouche \STR "abc" @ STR "xyz"\ +term_cartouche \STR "\"\ +term_cartouche \STR "\001\010\100"\ -subsection {* Proof method syntax *} +subsubsection {* Further nesting: antiquotations *} + +setup -- "ML antiquotation" +{* + ML_Antiquote.inline @{binding term_cartouche} + (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> + (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) +*} + +setup -- "document antiquotation" +{* + Thy_Output.antiquotation @{binding ML_cartouche} + (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn (txt, pos) => + let + val toks = + ML_Lex.read Position.none "fn _ => (" @ + ML_Lex.read pos txt @ + ML_Lex.read Position.none ");"; + val _ = ML_Context.eval_in (SOME context) false pos toks; + in "" end); +*} + +ML {* + @{term_cartouche \STR ""\}; + @{term_cartouche \STR "abc"\}; + @{term_cartouche \STR "abc" @ STR "xyz"\}; + @{term_cartouche \STR "\"\}; + @{term_cartouche \STR "\001\010\100"\}; +*} + +text {* + @{ML_cartouche + \ + ( + @{term_cartouche \STR ""\}; + @{term_cartouche \STR "abc"\}; + @{term_cartouche \STR "abc" @ STR "xyz"\}; + @{term_cartouche \STR "\"\}; + @{term_cartouche \STR "\001\010\100"\} + ) + \ + } +*} + + +subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *} + +ML {* + Outer_Syntax.command + @{command_spec "text_cartouche"} "" + (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup) +*} + +text_cartouche +\ + @{ML_cartouche + \ + ( + @{term_cartouche \STR ""\}; + @{term_cartouche \STR "abc"\}; + @{term_cartouche \STR "abc" @ STR "xyz"\}; + @{term_cartouche \STR "\"\}; + @{term_cartouche \STR "\001\010\100"\} + ) + \ + } +\ + + +subsection {* Proof method syntax: ML tactic expression *} ML {* structure ML_Tactic: @@ -83,7 +195,7 @@ *} -subsection {* Explicit version: method with cartouche argument *} +subsubsection {* Explicit version: method with cartouche argument *} method_setup ml_tactic = {* Scan.lift Args.cartouche_source_position @@ -104,7 +216,7 @@ text {* @{ML "@{lemma \"A \ B \ B \ A\" by (ml_tactic \blast_tac ctxt 1\)}"} *} -subsection {* Implicit version: method with special name "cartouche" (dynamic!) *} +subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *} method_setup "cartouche" = {* Scan.lift Args.cartouche_source_position diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/General/antiquote.ML Wed Jan 22 17:14:27 2014 +0100 @@ -45,20 +45,20 @@ val err_prefix = "Antiquotation lexical error: "; val scan_txt = - $$$ "@" --| Scan.ahead (~$$$ "{") || + $$$ "@" --| Scan.ahead (~$$ "{") || Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single; val scan_ant = Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || - Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 || + Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; in val scan_antiq = - Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- + Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") - (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) + (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat); diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/General/scan.ML Wed Jan 22 17:14:27 2014 +0100 @@ -64,6 +64,7 @@ val state: 'a * 'b -> 'a * ('a * 'b) val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e) val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd) + val provide: ('a -> bool) -> 'b -> ('b * 'c -> 'd * ('a * 'e)) -> 'c -> 'd * 'e val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c) val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd @@ -210,9 +211,11 @@ fun peek scan = depend (fn st => scan st >> pair st); -fun pass st scan xs = - let val (y, (_, xs')) = scan (st, xs) - in (y, xs') end; +fun provide pred st scan xs = + let val (y, (st', xs')) = scan (st, xs) + in if pred st' then (y, xs') else fail () end; + +fun pass st = provide (K true) st; fun lift scan (st, xs) = let val (y, xs') = scan xs diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/General/symbol_pos.ML Wed Jan 22 17:14:27 2014 +0100 @@ -8,6 +8,8 @@ sig type T = Symbol.symbol * Position.T val symbol: T -> Symbol.symbol + val $$ : Symbol.symbol -> T list -> T * T list + val ~$$ : Symbol.symbol -> T list -> T * T list val $$$ : Symbol.symbol -> T list -> T list * T list val ~$$$ : Symbol.symbol -> T list -> T list * T list val content: T list -> string @@ -26,16 +28,11 @@ val quote_string_q: string -> string val quote_string_qq: string -> string val quote_string_bq: string -> string - val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> - T list -> T list * T list - val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> - T list -> T list * T list + val scan_cartouche: string -> T list -> T list * T list val recover_cartouche: T list -> T list * T list val cartouche_content: T list -> T list - val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> - T list -> T list * T list - val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> - T list -> T list * T list + val scan_comment: string -> T list -> T list * T list + val scan_comment_body: string -> T list -> T list * T list val recover_comment: T list -> T list * T list val source: Position.T -> (Symbol.symbol, 'a) Source.source -> (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source @@ -91,6 +88,8 @@ fun change_prompt scan = Scan.prompt "# " scan; fun $$ s = Scan.one (fn x => symbol x = s); +fun ~$$ s = Scan.one (fn x => symbol x <> s); + fun $$$ s = Scan.one (fn x => symbol x = s) >> single; fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single; @@ -115,8 +114,10 @@ Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single; fun scan_strs q err_prefix = - (scan_pos --| $$$ q) -- !!! (fn () => err_prefix ^ "missing quote at end of string") - (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))); + Scan.ahead ($$ q) |-- + !!! (fn () => err_prefix ^ "unclosed string literal") + ((scan_pos --| $$$ q) -- + (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)))); fun recover_strs q = $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat); @@ -159,29 +160,20 @@ (* nested text cartouches *) -local - -val scan_cart = - Scan.depend (fn (d: int) => $$ "\\" >> pair (d + 1)) || - Scan.depend (fn 0 => Scan.fail | d => $$ "\\" >> pair (d - 1)) || - Scan.lift (Scan.one (fn (s, _) => s <> "\\" andalso Symbol.is_regular s)); - -val scan_carts = Scan.pass 0 (Scan.repeat scan_cart); - -val scan_body = change_prompt scan_carts; +val scan_cartouche_depth = + Scan.repeat1 (Scan.depend (fn (d: int) => + $$ "\\" >> pair (d + 1) || + (if d > 0 then + Scan.one (fn (s, _) => s <> "\\" andalso Symbol.is_regular s) >> pair d || + $$ "\\" >> pair (d - 1) + else Scan.fail))); -in - -fun scan_cartouche cut = - $$ "\\" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\"); +fun scan_cartouche err_prefix = + Scan.ahead ($$ "\\") |-- + !!! (fn () => err_prefix ^ "unclosed text cartouche") + (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth)); -fun scan_cartouche_body cut = - $$ "\\" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\"); - -val recover_cartouche = - $$$ "\\" @@@ scan_carts; - -end; +val recover_cartouche = Scan.pass 0 scan_cartouche_depth; fun cartouche_content syms = let @@ -214,11 +206,15 @@ in -fun scan_comment cut = - $$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")"); +fun scan_comment err_prefix = + Scan.ahead ($$ "(" -- $$ "*") |-- + !!! (fn () => err_prefix ^ "unclosed comment") + ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")"); -fun scan_comment_body cut = - $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")"); +fun scan_comment_body err_prefix = + Scan.ahead ($$ "(" -- $$ "*") |-- + !!! (fn () => err_prefix ^ "unclosed comment") + ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")"); val recover_comment = $$$ "(" @@@ $$$ "*" @@@ scan_cmts; @@ -284,6 +280,8 @@ structure Basic_Symbol_Pos = (*not open by default*) struct + val $$ = Symbol_Pos.$$; + val ~$$ = Symbol_Pos.~$$; val $$$ = Symbol_Pos.$$$; val ~$$$ = Symbol_Pos.~$$$; end; diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Isar/args.ML Wed Jan 22 17:14:27 2014 +0100 @@ -29,9 +29,9 @@ val bracks: 'a parser -> 'a parser val mode: string -> bool parser val maybe: 'a parser -> 'a option parser - val cartouche_source: string parser + val cartouche_inner_syntax: string parser val cartouche_source_position: (Symbol_Pos.text * Position.T) parser - val name_source: string parser + val name_inner_syntax: string parser val name_source_position: (Symbol_Pos.text * Position.T) parser val name: string parser val binding: binding parser @@ -151,10 +151,10 @@ fun maybe scan = $$$ "_" >> K NONE || scan >> SOME; val cartouche = token Parse.cartouche; -val cartouche_source = cartouche >> Token.source_of; +val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of; val cartouche_source_position = cartouche >> Token.source_position_of; -val name_source = named >> Token.source_of; +val name_inner_syntax = named >> Token.inner_syntax_of; val name_source_position = named >> Token.source_position_of; val name = named >> Token.content_of; @@ -182,11 +182,11 @@ val internal_attribute = value (fn Token.Attribute att => att); fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of); -fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of); -fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of); +fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of); +fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of); fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) || - alt_string >> evaluate Token.Fact (get o Token.source_of); + alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of); fun named_attribute att = internal_attribute || diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Isar/parse.ML Wed Jan 22 17:14:27 2014 +0100 @@ -167,7 +167,7 @@ fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap; fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of; -fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of; +fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of; fun kind k = group (fn () => Token.str_of_kind k) diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Isar/token.ML Wed Jan 22 17:14:27 2014 +0100 @@ -41,7 +41,7 @@ val is_space: T -> bool val is_blank: T -> bool val is_newline: T -> bool - val source_of: T -> string + val inner_syntax_of: T -> string val source_position_of: T -> Symbol_Pos.text * Position.T val content_of: T -> string val unparse: T -> string @@ -116,10 +116,10 @@ | TypeVar => "schematic type variable" | Nat => "natural number" | Float => "floating-point number" - | String => "string" + | String => "quoted string" | AltString => "back-quoted string" | Verbatim => "verbatim text" - | Cartouche => "cartouche" + | Cartouche => "text cartouche" | Space => "white space" | Comment => "comment text" | InternalValue => "internal value" @@ -206,7 +206,7 @@ (* token content *) -fun source_of (Token ((source, (pos, _)), (_, x), _)) = +fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) = if YXML.detect x then x else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source])); @@ -321,13 +321,15 @@ (* scan verbatim text *) val scan_verb = - $$$ "*" --| Scan.ahead (~$$$ "}") || + $$$ "*" --| Scan.ahead (~$$ "}") || Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single; val scan_verbatim = - (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text" - (Symbol_Pos.change_prompt - ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos))); + Scan.ahead ($$ "{" -- $$ "*") |-- + !!! "unclosed verbatim text" + ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- + Symbol_Pos.change_prompt + ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); val recover_verbatim = $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); @@ -336,7 +338,8 @@ (* scan cartouche *) val scan_cartouche = - Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos); + Symbol_Pos.scan_pos -- + ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *) @@ -351,7 +354,7 @@ (* scan comment *) val scan_comment = - Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos); + Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Wed Jan 22 17:14:27 2014 +0100 @@ -99,14 +99,14 @@ value (Binding.name "cpat") (Args.context -- - Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t => + Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); (* type classes *) -fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => +fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => Proof_Context.read_class ctxt s |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); @@ -116,13 +116,13 @@ inline (Binding.name "class_syntax") (class true) #> inline (Binding.name "sort") - (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => + (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); (* type constructors *) -fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source) +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) >> (fn (ctxt, (s, pos)) => let val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s; @@ -146,7 +146,7 @@ (* constants *) -fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source) +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) >> (fn (ctxt, (s, pos)) => let val Const (c, _) = Proof_Context.read_const_proper ctxt false s; @@ -169,7 +169,7 @@ else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> inline (Binding.name "const") - (Args.context -- Scan.lift Args.name_source -- Scan.optional + (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] >> (fn ((ctxt, raw_c), Ts) => let diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/ML/ml_lex.ML Wed Jan 22 17:14:27 2014 +0100 @@ -137,7 +137,9 @@ open Basic_Symbol_Pos; -fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg); +val err_prefix = "SML lexical error: "; + +fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* blanks *) @@ -241,8 +243,9 @@ $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; val scan_string = - $$$ "\"" @@@ !!! "missing quote at end of string" - ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\""); + Scan.ahead ($$ "\"") |-- + !!! "unclosed string literal" + ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\""); val recover_string = $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat); @@ -260,7 +263,7 @@ (scan_char >> token Char || scan_string >> token String || scan_blanks1 >> token Space || - Symbol_Pos.scan_comment !!! >> token Comment || + Symbol_Pos.scan_comment err_prefix >> token Comment || Scan.max token_leq (scan_keyword >> token Keyword) (scan_word >> token Word || @@ -304,9 +307,7 @@ (SOME (false, fn msg => recover msg >> map Antiquote.Text)) |> Source.exhaust |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token)) - |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))) - handle ERROR msg => - cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos); + |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))); in input @ termination end; end; diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Wed Jan 22 17:14:27 2014 +0100 @@ -85,7 +85,7 @@ val and_ = Args.$$$ "and"; val by = Args.$$$ "by"; -val goal = Scan.unless (by || and_) Args.name_source; +val goal = Scan.unless (by || and_) Args.name_inner_syntax; val _ = Theory.setup (ML_Context.add_antiq (Binding.name "lemma") diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Syntax/lexicon.ML Wed Jan 22 17:14:27 2014 +0100 @@ -24,8 +24,8 @@ val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val is_tid: string -> bool datatype token_kind = - Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | - NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF + Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | + FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF datatype token = Token of token_kind * string * Position.range val str_of_token: token -> string val pos_of_token: token -> Position.T @@ -42,8 +42,10 @@ val matching_tokens: token * token -> bool val valued_token: token -> bool val predef_term: string -> token option - val implode_str: string list -> string - val explode_str: string -> string list + val implode_string: Symbol.symbol list -> string + val explode_string: string * Position.T -> Symbol_Pos.T list + val implode_str: Symbol.symbol list -> string + val explode_str: string * Position.T -> Symbol_Pos.T list val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list val read_indexname: string -> indexname val read_var: string -> term @@ -87,7 +89,9 @@ open Basic_Symbol_Pos; -fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg); +val err_prefix = "Inner lexical error: "; + +fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); val scan_id = Symbol_Pos.scan_ident; val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat); @@ -114,8 +118,8 @@ (** datatype token **) datatype token_kind = - Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | - NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF; + Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | + FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF; datatype token = Token of token_kind * string * Position.range; @@ -150,6 +154,7 @@ ("float_token", FloatSy), ("xnum_token", XNumSy), ("str_token", StrSy), + ("string_token", StringSy), ("cartouche", Cartouche)]; val terminals = map #1 terminal_kinds; @@ -170,6 +175,7 @@ | FloatSy => Markup.numeral | XNumSy => Markup.numeral | StrSy => Markup.inner_string + | StringSy => Markup.inner_string | Cartouche => Markup.inner_cartouche | Comment => Markup.inner_comment | _ => Markup.empty; @@ -205,30 +211,45 @@ | NONE => NONE); -(* str tokens *) + +(** string literals **) + +fun explode_literal scan_body (str, pos) = + (case Scan.read Symbol_Pos.stopper scan_body (Symbol_Pos.explode (str, pos)) of + SOME ss => ss + | _ => error (err_prefix ^ "malformed string literal " ^ quote str ^ Position.here pos)); + + +(* string *) + +val scan_string = Scan.trace (Symbol_Pos.scan_string_qq err_prefix) >> #2; +val scan_string_body = Symbol_Pos.scan_string_qq err_prefix >> (#1 o #2); + +fun implode_string ss = quote (implode (map (fn "\"" => "\\\"" | s => s) ss)); +val explode_string = explode_literal scan_string_body; + + +(* str *) val scan_chr = - $$$ "\\" |-- $$$ "'" || + $$ "\\" |-- $$$ "'" || Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o Symbol_Pos.symbol) >> single || - $$$ "'" --| Scan.ahead (~$$$ "'"); + $$$ "'" --| Scan.ahead (~$$ "'"); val scan_str = - $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string" - ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'"); + Scan.ahead ($$ "'" -- $$ "'") |-- + !!! "unclosed string literal" + ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'"); val scan_str_body = - $$$ "'" |-- $$$ "'" |-- !!! "missing end of string" - ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'"); - + Scan.ahead ($$ "'" |-- $$ "'") |-- + !!! "unclosed string literal" + ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'"); -fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); - -fun explode_str str = - (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of - SOME cs => map Symbol_Pos.symbol cs - | _ => error ("Inner lexical error: literal string expected at " ^ quote str)); +fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss)); +val explode_str = explode_literal scan_str_body; @@ -258,17 +279,18 @@ val scan_lit = Scan.literal lex >> token Literal; val scan_token = - Symbol_Pos.scan_cartouche !!! >> token Cartouche || - Symbol_Pos.scan_comment !!! >> token Comment || + Symbol_Pos.scan_cartouche err_prefix >> token Cartouche || + Symbol_Pos.scan_comment err_prefix >> token Comment || Scan.max token_leq scan_lit scan_val || + scan_string >> token StringSy || scan_str >> token StrSy || Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space; in (case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of (toks, []) => toks - | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^ - Position.here (#1 (Symbol_Pos.range ss)))) + | (_, ss) => + error (err_prefix ^ Symbol_Pos.content ss ^ Position.here (#1 (Symbol_Pos.range ss)))) end; @@ -293,7 +315,7 @@ val scan = (scan_id >> map Symbol_Pos.symbol) -- - Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1; + Scan.optional ($$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1; in scan >> (fn (cs, ~1) => chop_idx (rev cs) [] @@ -302,7 +324,7 @@ in -val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname; +val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname; end; @@ -320,7 +342,7 @@ fun read_var str = let val scan = - $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) + $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> Syntax.var || Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (Syntax.free o implode o map Symbol_Pos.symbol); @@ -330,7 +352,7 @@ (* read_variable *) fun read_variable str = - let val scan = $$$ "?" |-- scan_indexname || scan_indexname + let val scan = $$ "?" |-- scan_indexname || scan_indexname in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end; diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Wed Jan 22 17:14:27 2014 +0100 @@ -570,9 +570,9 @@ basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #> basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #> basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #> - basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #> + basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #> basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #> - basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #> + basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #> basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #> basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #> basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #> diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Tools/rail.ML Wed Jan 22 17:14:27 2014 +0100 @@ -266,7 +266,7 @@ val _ = Theory.setup (Thy_Output.antiquotation @{binding rail} - (Scan.lift (Parse.source_position Parse.string)) + (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche))) (fn {state, ...} => output_rules state o read)); end; diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/Tools/rule_insts.ML Wed Jan 22 17:14:27 2014 +0100 @@ -165,7 +165,7 @@ val _ = Theory.setup (Attrib.setup @{binding "where"} - (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >> + (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >> (fn args => Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) "named instantiation of theorem"); @@ -175,7 +175,7 @@ local -val inst = Args.maybe Args.name_source; +val inst = Args.maybe Args.name_inner_syntax; val concl = Args.$$$ "concl" -- Args.colon; val insts = @@ -320,7 +320,7 @@ fun method inst_tac tac = Args.goal_spec -- Scan.optional (Scan.lift - (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --| + (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --| Args.$$$ "in")) [] -- Attrib.thms >> (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts => @@ -347,12 +347,12 @@ Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac)) "cut rule (dynamic instantiation)" #> Method.setup @{binding subgoal_tac} - (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >> + (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >> (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props)))) "insert subgoal (dynamic instantiation)" #> Method.setup @{binding thin_tac} - (Args.goal_spec -- Scan.lift Args.name_source >> + (Args.goal_spec -- Scan.lift Args.name_inner_syntax >> (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop))) "remove premise (dynamic instantiation)"); diff -r 761e40ce91bc -r 0ee5c17f2207 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Pure/pure_thy.ML Wed Jan 22 17:14:27 2014 +0100 @@ -70,8 +70,9 @@ "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", "any", "prop'", "num_const", "float_const", "xnum_const", "num_position", "float_position", "xnum_position", "index", "struct", "tid_position", - "tvar_position", "id_position", "longid_position", "var_position", "str_position", - "cartouche_position", "type_name", "class_name"])) + "tvar_position", "id_position", "longid_position", "var_position", + "str_position", "string_position", "cartouche_position", "type_name", + "class_name"])) #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers) #> Sign.add_syntax_i [("", typ "prop' => prop", Delimfix "_"), @@ -155,6 +156,7 @@ ("_position", typ "longid => longid_position", Delimfix "_"), ("_position", typ "var => var_position", Delimfix "_"), ("_position", typ "str_token => str_position", Delimfix "_"), + ("_position", typ "string_token => string_position", Delimfix "_"), ("_position", typ "cartouche => cartouche_position", Delimfix "_"), ("_type_constraint_", typ "'a", NoSyn), ("_context_const", typ "id_position => logic", Delimfix "CONST _"), diff -r 761e40ce91bc -r 0ee5c17f2207 src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/Tools/induct_tacs.ML Wed Jan 22 17:14:27 2014 +0100 @@ -122,13 +122,14 @@ val opt_rules = Scan.option (rule_spec |-- Attrib.thms); val varss = - Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source)))); + Parse.and_list' + (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax)))); in val setup = Method.setup @{binding case_tac} - (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >> + (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >> (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r))) "unstructured case analysis on types" #> Method.setup @{binding induct_tac} diff -r 761e40ce91bc -r 0ee5c17f2207 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Wed Jan 22 10:13:40 2014 +0100 +++ b/src/ZF/Tools/ind_cases.ML Wed Jan 22 17:14:27 2014 +0100 @@ -57,7 +57,7 @@ val setup = Method.setup @{binding "ind_cases"} - (Scan.lift (Scan.repeat1 Args.name_source) >> + (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >> (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props))) "dynamic case analysis on sets"; diff -r 761e40ce91bc -r 0ee5c17f2207 src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/ZF/UNITY/SubstAx.thy Wed Jan 22 17:14:27 2014 +0100 @@ -375,7 +375,7 @@ *} method_setup ensures = {* - Args.goal_spec -- Scan.lift Args.name_source >> + Args.goal_spec -- Scan.lift Args.name_inner_syntax >> (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) *} "for proving progress properties"