src/Pure/Isar/outer_parse.ML
changeset 15703 727ef1b8b3ee
parent 15570 8d8c70b41bab
child 15714 9b8da47715c3
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -14,9 +14,7 @@
     1.4    val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
     1.5    val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
     1.6    val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
     1.7 -  val $$$ : string -> token list -> string * token list
     1.8 -  val semicolon: token list -> string * token list
     1.9 -  val underscore: token list -> string * token list
    1.10 +  val not_eof: token list -> token * token list
    1.11    val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
    1.12    val command: token list -> string * token list
    1.13    val keyword: token list -> string * token list
    1.14 @@ -31,7 +29,10 @@
    1.15    val verbatim: token list -> string * token list
    1.16    val sync: token list -> string * token list
    1.17    val eof: token list -> string * token list
    1.18 -  val not_eof: token list -> token * token list
    1.19 +  val $$$ : string -> token list -> string * token list
    1.20 +  val semicolon: token list -> string * token list
    1.21 +  val underscore: token list -> string * token list
    1.22 +  val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
    1.23    val opt_unit: token list -> unit * token list
    1.24    val opt_keyword: string -> token list -> bool * token list
    1.25    val nat: token list -> int * token list
    1.26 @@ -45,7 +46,6 @@
    1.27    val xname: token list -> xstring * token list
    1.28    val text: token list -> string * token list
    1.29    val path: token list -> Path.T * token list
    1.30 -  val uname: token list -> string option * token list
    1.31    val sort: token list -> string * token list
    1.32    val arity: token list -> (string list * string) * token list
    1.33    val type_args: token list -> string list * token list
    1.34 @@ -61,19 +61,19 @@
    1.35    val propp: token list -> (string * (string list * string list)) * token list
    1.36    val termp: token list -> (string * string list) * token list
    1.37    val arguments: token list -> Args.T list * token list
    1.38 -  val attribs: token list -> Args.src list * token list
    1.39 -  val opt_attribs: token list -> Args.src list * token list
    1.40 -  val thm_name: string -> token list -> (bstring * Args.src list) * token list
    1.41 -  val opt_thm_name: string -> token list -> (bstring * Args.src list) * token list
    1.42 -  val spec_name: token list -> ((bstring * string) * Args.src list) * token list
    1.43 -  val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
    1.44 -  val xthm: token list -> (thmref * Args.src list) * token list
    1.45 -  val xthms1: token list -> (thmref * Args.src list) list * token list
    1.46 +  val attribs: token list -> Attrib.src list * token list
    1.47 +  val opt_attribs: token list -> Attrib.src list * token list
    1.48 +  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    1.49 +  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    1.50 +  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.51 +  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.52 +  val xthm: token list -> (thmref * Attrib.src list) * token list
    1.53 +  val xthms1: token list -> (thmref * Attrib.src list) list * token list
    1.54    val locale_target: token list -> xstring option * token list
    1.55    val locale_expr: token list -> Locale.expr * token list
    1.56    val locale_keyword: token list -> string * token list
    1.57 -  val locale_element: token list -> Args.src Locale.element * token list
    1.58 -  val locale_elem_or_expr: token list -> Args.src Locale.element Locale.elem_expr * token list
    1.59 +  val locale_element: token list -> Locale.element * token list
    1.60 +  val locale_elem_or_expr: token list -> Locale.element Locale.elem_expr * token list
    1.61    val method: token list -> Method.text * token list
    1.62  end;
    1.63  
    1.64 @@ -122,8 +122,9 @@
    1.65  
    1.66  (* tokens *)
    1.67  
    1.68 -fun position scan =
    1.69 -  (Scan.ahead (Scan.one T.not_eof) >> T.position_of) -- scan >> Library.swap;
    1.70 +val not_eof = Scan.one T.not_eof;
    1.71 +
    1.72 +fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
    1.73  
    1.74  fun kind k =
    1.75    group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);
    1.76 @@ -148,13 +149,12 @@
    1.77  
    1.78  val semicolon = $$$ ";";
    1.79  
    1.80 +val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
    1.81  val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
    1.82 -val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
    1.83 +fun maybe scan = underscore >> K NONE || scan >> SOME;
    1.84  
    1.85  val nat = number >> (#1 o Library.read_int o Symbol.explode);
    1.86  
    1.87 -val not_eof = Scan.one T.not_eof;
    1.88 -
    1.89  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
    1.90  
    1.91  fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
    1.92 @@ -179,8 +179,6 @@
    1.93  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    1.94  val path = group "file name/path specification" name >> Path.unpack;
    1.95  
    1.96 -val uname = underscore >> K NONE || name >> SOME;
    1.97 -
    1.98  
    1.99  (* sorts and arities *)
   1.100  
   1.101 @@ -265,13 +263,13 @@
   1.102  fun atom_arg is_symid blk =
   1.103    group "argument"
   1.104      (position (short_ident || long_ident || sym_ident || term_var ||
   1.105 -        type_ident || type_var || number) >> Args.ident ||
   1.106 -      position (keyword_symid is_symid) >> Args.keyword ||
   1.107 -      position (string || verbatim) >> Args.string ||
   1.108 -      position (if blk then $$$ "," else Scan.fail) >> Args.keyword);
   1.109 +        type_ident || type_var || number) >> Args.mk_ident ||
   1.110 +      position (keyword_symid is_symid) >> Args.mk_keyword ||
   1.111 +      position (string || verbatim) >> Args.mk_string ||
   1.112 +      position (if blk then $$$ "," else Scan.fail) >> Args.mk_keyword);
   1.113  
   1.114  fun paren_args l r scan = position ($$$ l) -- !!! (scan true -- position ($$$ r))
   1.115 -  >> (fn (x, (ys, z)) => Args.keyword x :: ys @ [Args.keyword z]);
   1.116 +  >> (fn (x, (ys, z)) => Args.mk_keyword x :: ys @ [Args.mk_keyword z]);
   1.117  
   1.118  fun args is_symid blk x = Scan.optional (args1 is_symid blk) [] x
   1.119  and args1 is_symid blk x =
   1.120 @@ -297,8 +295,9 @@
   1.121  val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
   1.122  
   1.123  val thm_sel = $$$ "(" |-- list1
   1.124 -  (   nat --| minus -- nat >> op upto
   1.125 -   || nat >> single) --| $$$ ")" >> List.concat;
   1.126 + (nat --| minus -- nat >> PureThy.FromTo ||
   1.127 +  nat --| minus >> PureThy.From ||
   1.128 +  nat >> PureThy.Single) --| $$$ ")";
   1.129  
   1.130  val xthm = xname -- Scan.option thm_sel -- opt_attribs;
   1.131  val xthms1 = Scan.repeat1 xthm;
   1.132 @@ -325,7 +324,7 @@
   1.133    scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
   1.134  
   1.135  fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
   1.136 -and expr1 x = (expr2 -- Scan.repeat1 uname >> Locale.Rename || expr2) x
   1.137 +and expr1 x = (expr2 -- Scan.repeat1 (maybe name) >> Locale.Rename || expr2) x
   1.138  and expr0 x = (plus1 expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
   1.139  
   1.140  in