# HG changeset patch # User wenzelm # Date 1365504986 -7200 # Node ID 8450b944e58a0f705592505493f530f1647b30d5 # Parent 97de25c51b2df954930077c058ea096f632dd9ed just one syntax category "mixfix" -- check structure annotation semantically; diff -r 97de25c51b2d -r 8450b944e58a src/Doc/IsarRef/Inner_Syntax.thy --- a/src/Doc/IsarRef/Inner_Syntax.thy Tue Apr 09 12:29:36 2013 +0200 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Tue Apr 09 12:56:26 2013 +0200 @@ -362,14 +362,12 @@ than the fixity declarations of ML and Prolog. @{rail " - @{syntax_def mixfix}: '(' mfix ')' - ; - @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')' - ; - - mfix: @{syntax template} prios? @{syntax nat}? | + @{syntax_def mixfix}: '(' + @{syntax template} prios? @{syntax nat}? | (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} | - @'binder' @{syntax template} prios? @{syntax nat} + @'binder' @{syntax template} prios? @{syntax nat} | + @'structure' + ')' ; template: string ; @@ -379,9 +377,9 @@ The string given as @{text template} may include literal text, spacing, blocks, and arguments (denoted by ``@{text _}''); the special symbol ``@{verbatim "\"}'' (printed as ``@{text "\"}'') - represents an index argument that specifies an implicit structure - reference (see also \secref{sec:locale}). Infix and binder - declarations provide common abbreviations for particular mixfix + represents an index argument that specifies an implicit + @{text "\"} reference (see also \secref{sec:locale}). Infix and + binder declarations provide common abbreviations for particular mixfix declarations. So in practice, mixfix templates mostly degenerate to literal text for concrete syntax, such as ``@{verbatim "++"}'' for an infix symbol. @@ -568,9 +566,9 @@ @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and') ; (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\ - (@{syntax nameref} @{syntax struct_mixfix} + @'and') + (@{syntax nameref} @{syntax mixfix} + @'and') ; - @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and') + @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and') "} \begin{description} diff -r 97de25c51b2d -r 8450b944e58a src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Apr 09 12:29:36 2013 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Apr 09 12:56:26 2013 +0200 @@ -208,13 +208,13 @@ val _ = Outer_Syntax.local_theory @{command_spec "notation"} "add concrete syntax for constants / fixed variables" - (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix) + (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = Outer_Syntax.local_theory @{command_spec "no_notation"} "delete concrete syntax for constants / fixed variables" - (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix) + (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); @@ -604,7 +604,7 @@ val _ = Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables" - (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix) + (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args))); val case_spec = diff -r 97de25c51b2d -r 8450b944e58a src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Tue Apr 09 12:29:36 2013 +0200 +++ b/src/Pure/Isar/parse.ML Tue Apr 09 12:56:26 2013 +0200 @@ -298,6 +298,8 @@ (* mixfix annotations *) +local + val mfix = string -- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000) >> (Mixfix o triple2); @@ -305,18 +307,25 @@ val infx = $$$ "infix" |-- !!! (string -- nat >> Infix); val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl); val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr); +val strcture = $$$ "structure" >> K Structure; val binder = $$$ "binder" |-- !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n)))) >> (Binder o triple2); -fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")"); -fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn; +val mixfix_body = mfix || strcture || binder || infxl || infxr || infx; + +fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")"); +fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn; + +in -val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx); -val mixfix' = annotation I (mfix || binder || infxl || infxr || infx); -val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx); -val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx); +val mixfix = annotation !!! mixfix_body; +val mixfix' = annotation I mixfix_body; +val opt_mixfix = opt_annotation !!! mixfix_body; +val opt_mixfix' = opt_annotation I mixfix_body; + +end; (* fixes *) diff -r 97de25c51b2d -r 8450b944e58a src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Tue Apr 09 12:29:36 2013 +0200 +++ b/src/Pure/Isar/parse_spec.ML Tue Apr 09 12:56:26 2013 +0200 @@ -20,7 +20,6 @@ val constdecl: (binding * string option * mixfix) parser val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser val includes: (xstring * Position.T) list parser - val locale_mixfix: mixfix parser val locale_fixes: (binding * string option * mixfix) list parser val locale_insts: (string option list * (Attrib.binding * string) list) parser val class_expression: string list parser @@ -83,12 +82,8 @@ val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname)); -val locale_mixfix = - Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure || - Parse.mixfix; - val locale_fixes = - Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix + Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix >> (single o Parse.triple1) || Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;