author  wenzelm 
Fri, 03 Apr 2015 20:04:16 +0200  
changeset 59918  d01e6d159c33 
parent 59917  9830c944670f 
child 59924  801b979ec0c2 
permissions  rwrr 
36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
35838
diff
changeset

1 
(* Title: Pure/Isar/parse.ML 
5826  2 
Author: Markus Wenzel, TU Muenchen 
3 

4 
Generic parsers for Isabelle/Isar outer syntax. 

5 
*) 

6 

36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
35838
diff
changeset

7 
signature PARSE = 
5826  8 
sig 
44357  9 
val group: (unit > string) > (Token.T list > 'a) > Token.T list > 'a 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

10 
val !!! : (Token.T list > 'a) > Token.T list > 'a 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

11 
val !!!! : (Token.T list > 'a) > Token.T list > 'a 
12047  12 
val triple1: ('a * 'b) * 'c > 'a * 'b * 'c 
13 
val triple2: 'a * ('b * 'c) > 'a * 'b * 'c 

14 
val triple_swap: ('a * 'b) * 'c > ('a * 'c) * 'b 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

15 
val not_eof: Token.T parser 
56201  16 
val token: 'a parser > Token.T parser 
59029
c907cbe36713
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58908
diff
changeset

17 
val range: 'a parser > ('a * Position.range) parser 
42326  18 
val position: 'a parser > ('a * Position.T) parser 
59809  19 
val input: 'a parser > Input.source parser 
42326  20 
val inner_syntax: 'a parser > string parser 
58908  21 
val command_: string parser 
29310  22 
val keyword: string parser 
23 
val short_ident: string parser 

24 
val long_ident: string parser 

25 
val sym_ident: string parser 

26 
val minus: string parser 

27 
val term_var: string parser 

28 
val type_ident: string parser 

29 
val type_var: string parser 

30 
val number: string parser 

40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
36959
diff
changeset

31 
val float_number: string parser 
29310  32 
val string: string parser 
33 
val alt_string: string parser 

34 
val verbatim: string parser 

55033  35 
val cartouche: string parser 
29310  36 
val eof: string parser 
58908  37 
val command: string > string parser 
29310  38 
val keyword_with: (string > bool) > string parser 
56202  39 
val keyword_markup: bool * Markup.T > string > string parser 
40 
val keyword_improper: string > string parser 

29310  41 
val $$$ : string > string parser 
42 
val reserved: string > string parser 

43 
val underscore: string parser 

44 
val maybe: 'a parser > 'a option parser 

45 
val tag_name: string parser 

46 
val tags: string list parser 

47 
val opt_keyword: string > bool parser 

59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59809
diff
changeset

48 
val opt_bang: bool parser 
29310  49 
val begin: string parser 
50 
val opt_begin: bool parser 

51 
val nat: int parser 

52 
val int: int parser 

40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
36959
diff
changeset

53 
val real: real parser 
55764  54 
val enum_positions: string > 'a parser > ('a list * Position.T list) parser 
55 
val enum1_positions: string > 'a parser > ('a list * Position.T list) parser 

29310  56 
val enum: string > 'a parser > 'a list parser 
57 
val enum1: string > 'a parser > 'a list parser 

58 
val and_list: 'a parser > 'a list parser 

59 
val and_list1: 'a parser > 'a list parser 

30511  60 
val enum': string > 'a context_parser > 'a list context_parser 
61 
val enum1': string > 'a context_parser > 'a list context_parser 

62 
val and_list': 'a context_parser > 'a list context_parser 

63 
val and_list1': 'a context_parser > 'a list context_parser 

29310  64 
val list: 'a parser > 'a list parser 
65 
val list1: 'a parser > 'a list parser 

43775
b361c7d184e7
added Parse.properties (again)  allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
wenzelm
parents:
42657
diff
changeset

66 
val properties: Properties.T parser 
29310  67 
val name: bstring parser 
29581  68 
val binding: binding parser 
29310  69 
val xname: xstring parser 
70 
val text: string parser 

48881
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
46922
diff
changeset

71 
val path: string parser 
59693  72 
val theory_name: bstring parser 
73 
val theory_xname: xstring parser 

40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40793
diff
changeset

74 
val liberal_name: xstring parser 
29310  75 
val parname: string parser 
29581  76 
val parbinding: binding parser 
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

77 
val class: string parser 
29310  78 
val sort: string parser 
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

79 
val type_const: string parser 
29310  80 
val arity: (string * string list * string) parser 
81 
val multi_arity: (string list * string list * string) parser 

82 
val type_args: string list parser 

35838  83 
val type_args_constrained: (string * string option) list parser 
29310  84 
val typ_group: string parser 
85 
val typ: string parser 

86 
val mixfix: mixfix parser 

87 
val mixfix': mixfix parser 

88 
val opt_mixfix: mixfix parser 

89 
val opt_mixfix': mixfix parser 

90 
val where_: string parser 

42299  91 
val const_decl: (string * string * mixfix) parser 
30339  92 
val const_binding: (binding * string * mixfix) parser 
29581  93 
val params: (binding * string option) list parser 
94 
val fixes: (binding * string option * mixfix) list parser 

95 
val for_fixes: (binding * string option * mixfix) list parser 

59064  96 
val ML_source: Input.source parser 
97 
val document_source: Input.source parser 

29310  98 
val term_group: string parser 
99 
val prop_group: string parser 

100 
val term: string parser 

101 
val prop: string parser 

42300
0d1cbc1fe579
notation: proper markup for type constructor / constant;
wenzelm
parents:
42299
diff
changeset

102 
val const: string parser 
40793
d21aedaa91e7
added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents:
40296
diff
changeset

103 
val literal_fact: string parser 
29310  104 
val propp: (string * string list) parser 
105 
val termp: (string * string list) parser 

45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45331
diff
changeset

106 
val target: (xstring * Position.T) parser 
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45331
diff
changeset

107 
val opt_target: (xstring * Position.T) option parser 
56201  108 
val args: Token.T list parser 
109 
val args1: (string > bool) > Token.T list parser 

58028
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

110 
val attribs: Token.src list parser 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

111 
val opt_attribs: Token.src list parser 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

112 
val thm_sel: Facts.interval list parser 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

113 
val xthm: (Facts.ref * Token.src list) parser 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

114 
val xthms1: (Facts.ref * Token.src list) list parser 
5826  115 
end; 
116 

36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
35838
diff
changeset

117 
structure Parse: PARSE = 
5826  118 
struct 
119 

120 
(** error handling **) 

121 

122 
(* group atomic parsers (no cuts!) *) 

123 

44357  124 
fun group s scan = scan  Scan.fail_with 
48911
5debc3e4fa81
tuned messages: endofinput rarely means physical endoffile from the past;
wenzelm
parents:
48881
diff
changeset

125 
(fn [] => (fn () => s () ^ " expected,\nbut endofinput was found") 
42519  126 
 tok :: _ => 
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

127 
(fn () => 
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

128 
(case Token.text_of tok of 
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

129 
(txt, "") => 
55708  130 
s () ^ " expected,\nbut " ^ txt ^ Position.here (Token.pos_of tok) ^ 
131 
" was found" 

43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

132 
 (txt1, txt2) => 
55708  133 
s () ^ " expected,\nbut " ^ txt1 ^ Position.here (Token.pos_of tok) ^ 
134 
" was found:\n" ^ txt2))); 

5826  135 

136 

5877  137 
(* cut *) 
5826  138 

8581
5c7ed2af8bfb
!!!! = cut "Corrupted outer syntax in presentation";
wenzelm
parents:
8350
diff
changeset

139 
fun cut kind scan = 
5826  140 
let 
48911
5debc3e4fa81
tuned messages: endofinput rarely means physical endoffile from the past;
wenzelm
parents:
48881
diff
changeset

141 
fun get_pos [] = " (endofinput)" 
55708  142 
 get_pos (tok :: _) = Position.here (Token.pos_of tok); 
5826  143 

43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

144 
fun err (toks, NONE) = (fn () => kind ^ get_pos toks) 
25625  145 
 err (toks, SOME msg) = 
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

146 
(fn () => 
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

147 
let val s = msg () in 
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

148 
if String.isPrefix kind s then s 
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

149 
else kind ^ get_pos toks ^ ": " ^ s 
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43775
diff
changeset

150 
end); 
5826  151 
in Scan.!! err scan end; 
152 

8586  153 
fun !!! scan = cut "Outer syntax error" scan; 
154 
fun !!!! scan = cut "Corrupted outer syntax in presentation" scan; 

8581
5c7ed2af8bfb
!!!! = cut "Corrupted outer syntax in presentation";
wenzelm
parents:
8350
diff
changeset

155 

5826  156 

157 

158 
(** basic parsers **) 

159 

160 
(* utils *) 

161 

162 
fun triple1 ((x, y), z) = (x, y, z); 

163 
fun triple2 (x, (y, z)) = (x, y, z); 

6430  164 
fun triple_swap ((x, y), z) = ((x, z), y); 
5826  165 

166 

167 
(* tokens *) 

168 

27815  169 
fun RESET_VALUE atom = (*required for all primitive parsers*) 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

170 
Scan.ahead (Scan.one (K true))  atom >> (fn (arg, x) => (Token.assign NONE arg; x)); 
27815  171 

172 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

173 
val not_eof = RESET_VALUE (Scan.one Token.not_eof); 
15703  174 

56201  175 
fun token atom = Scan.ahead not_eof  atom; 
176 

59029
c907cbe36713
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58908
diff
changeset

177 
fun range scan = (Scan.ahead not_eof >> (Token.range_of o single))  scan >> Library.swap; 
55708  178 
fun position scan = (Scan.ahead not_eof >> Token.pos_of)  scan >> Library.swap; 
59809  179 
fun input atom = Scan.ahead atom  not_eof >> Token.input_of; 
55111  180 
fun inner_syntax atom = Scan.ahead atom  not_eof >> Token.inner_syntax_of; 
5826  181 

182 
fun kind k = 

44357  183 
group (fn () => Token.str_of_kind k) 
184 
(RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of)); 

5826  185 

58908  186 
val command_ = kind Token.Command; 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

187 
val keyword = kind Token.Keyword; 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

188 
val short_ident = kind Token.Ident; 
59081  189 
val long_ident = kind Token.Long_Ident; 
190 
val sym_ident = kind Token.Sym_Ident; 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

191 
val term_var = kind Token.Var; 
59081  192 
val type_ident = kind Token.Type_Ident; 
193 
val type_var = kind Token.Type_Var; 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

194 
val number = kind Token.Nat; 
40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
36959
diff
changeset

195 
val float_number = kind Token.Float; 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

196 
val string = kind Token.String; 
59081  197 
val alt_string = kind Token.Alt_String; 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

198 
val verbatim = kind Token.Verbatim; 
55033  199 
val cartouche = kind Token.Cartouche; 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

200 
val eof = kind Token.EOF; 
5826  201 

58908  202 
fun command x = 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48911
diff
changeset

203 
group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48911
diff
changeset

204 
(RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x))) 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48911
diff
changeset

205 
>> Token.content_of; 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48911
diff
changeset

206 

56202  207 
fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of); 
208 

209 
fun keyword_markup markup x = 

44357  210 
group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x) 
56063  211 
(Scan.ahead not_eof  keyword_with (fn y => x = y)) 
56202  212 
>> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x)); 
213 

214 
val keyword_improper = keyword_markup (true, Markup.improper); 

215 
val $$$ = keyword_markup (false, Markup.quasi_keyword); 

9131  216 

16030  217 
fun reserved x = 
44357  218 
group (fn () => "reserved identifier " ^ quote x) 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

219 
(RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of)); 
16030  220 

15703  221 
val minus = sym_ident : (fn "" => Scan.succeed ()  _ => Scan.fail) >> #1; 
11792
311eee3d63b6
parser for underscore (actually a symbolic identifier!);
wenzelm
parents:
11651
diff
changeset

222 
val underscore = sym_ident : (fn "_" => Scan.succeed ()  _ => Scan.fail) >> #1; 
15703  223 
fun maybe scan = underscore >> K NONE  scan >> SOME; 
11792
311eee3d63b6
parser for underscore (actually a symbolic identifier!);
wenzelm
parents:
11651
diff
changeset

224 

14835  225 
val nat = number >> (#1 o Library.read_int o Symbol.explode); 
27815  226 
val int = Scan.optional (minus >> K ~1) 1  nat >> op *; 
51988  227 
val real = float_number >> Markup.parse_real  int >> Real.fromInt; 
5826  228 

44357  229 
val tag_name = group (fn () => "tag name") (short_ident  string); 
17070  230 
val tags = Scan.repeat ($$$ "%"  !!! tag_name); 
231 

14646  232 
fun opt_keyword s = Scan.optional ($$$ "("  !!! (($$$ s >> K true)  $$$ ")")) false; 
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59809
diff
changeset

233 
val opt_bang = Scan.optional ($$$ "!" >> K true) false; 
14646  234 

20983  235 
val begin = $$$ "begin"; 
236 
val opt_begin = Scan.optional (begin >> K true) false; 

20961  237 

5826  238 

239 
(* enumerations *) 

240 

55764  241 
fun enum1_positions sep scan = 
242 
scan  Scan.repeat (position ($$$ sep)  !!! scan) >> 

243 
(fn (x, ys) => (x :: map #2 ys, map (#2 o #1) ys)); 

244 
fun enum_positions sep scan = 

245 
enum1_positions sep scan  Scan.succeed ([], []); 

246 

25999  247 
fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep  !!! scan); 
5826  248 
fun enum sep scan = enum1 sep scan  Scan.succeed []; 
249 

27815  250 
fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep)  scan); 
251 
fun enum' sep scan = enum1' sep scan  Scan.succeed []; 

5826  252 

6013  253 
fun and_list1 scan = enum1 "and" scan; 
254 
fun and_list scan = enum "and" scan; 

255 

27815  256 
fun and_list1' scan = enum1' "and" scan; 
257 
fun and_list' scan = enum' "and" scan; 

258 

259 
fun list1 scan = enum1 "," scan; 

260 
fun list scan = enum "," scan; 

261 

43775
b361c7d184e7
added Parse.properties (again)  allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
wenzelm
parents:
42657
diff
changeset

262 
val properties = $$$ "("  !!! (list (string  ($$$ "="  string))  $$$ ")"); 
b361c7d184e7
added Parse.properties (again)  allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
wenzelm
parents:
42657
diff
changeset

263 

5826  264 

5960  265 
(* names and text *) 
5826  266 

44357  267 
val name = group (fn () => "name declaration") (short_ident  sym_ident  string  number); 
268 

30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
29581
diff
changeset

269 
val binding = position name >> Binding.make; 
44357  270 

271 
val xname = group (fn () => "name reference") 

272 
(short_ident  long_ident  sym_ident  string  number); 

273 

274 
val text = group (fn () => "text") 

56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56202
diff
changeset

275 
(short_ident  long_ident  sym_ident  string  number  verbatim  cartouche); 
44357  276 

48881
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
46922
diff
changeset

277 
val path = group (fn () => "file name/path specification") name; 
6553  278 

59693  279 
val theory_name = group (fn () => "theory name") name; 
280 
val theory_xname = group (fn () => "theory name reference") xname; 

281 

56063  282 
val liberal_name = keyword_with Token.ident_or_symbolic  xname; 
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40793
diff
changeset

283 

18898  284 
val parname = Scan.optional ($$$ "("  name  $$$ ")") ""; 
28965  285 
val parbinding = Scan.optional ($$$ "("  binding  $$$ ")") Binding.empty; 
18898  286 

6553  287 

46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

288 
(* type classes *) 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

289 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

290 
val class = group (fn () => "type class") (inner_syntax xname); 
5826  291 

44357  292 
val sort = group (fn () => "sort") (inner_syntax xname); 
5826  293 

46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

294 
val type_const = inner_syntax (group (fn () => "type constructor") xname); 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

295 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

296 
val arity = type_const  ($$$ "::"  !!! 
22331  297 
(Scan.optional ($$$ "("  !!! (list1 sort  $$$ ")")) []  sort)) >> triple2; 
5826  298 

46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45596
diff
changeset

299 
val multi_arity = and_list1 type_const  ($$$ "::"  !!! 
25541  300 
(Scan.optional ($$$ "("  !!! (list1 sort  $$$ ")")) []  sort)) >> triple2; 
301 

5826  302 

303 
(* types *) 

304 

44357  305 
val typ_group = 
306 
group (fn () => "type") 

307 
(short_ident  long_ident  sym_ident  type_ident  type_var  string  number); 

5826  308 

27753
94b672153b49
sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents:
27737
diff
changeset

309 
val typ = inner_syntax typ_group; 
94b672153b49
sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents:
27737
diff
changeset

310 

35838  311 
fun type_arguments arg = 
312 
arg >> single  

313 
$$$ "("  !!! (list1 arg  $$$ ")")  

5826  314 
Scan.succeed []; 
315 

35838  316 
val type_args = type_arguments type_ident; 
317 
val type_args_constrained = type_arguments (type_ident  Scan.option ($$$ "::"  !!! sort)); 

318 

5826  319 

320 
(* mixfix annotations *) 

321 

51654
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

322 
local 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

323 

18669  324 
val mfix = string  
325 
!!! (Scan.optional ($$$ "["  !!! (list nat  $$$ "]")) []  

42297
140f283266b7
discontinued Syntax.max_pri, which is not really a symbolic parameter;
wenzelm
parents:
42287
diff
changeset

326 
Scan.optional nat 1000) >> (Mixfix o triple2); 
18669  327 

35130  328 
val infx = $$$ "infix"  !!! (string  nat >> Infix); 
329 
val infxl = $$$ "infixl"  !!! (string  nat >> Infixl); 

330 
val infxr = $$$ "infixr"  !!! (string  nat >> Infixr); 

51654
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

331 
val strcture = $$$ "structure" >> K Structure; 
5826  332 

18669  333 
val binder = $$$ "binder"  
334 
!!! (string  ($$$ "["  nat  $$$ "]"  nat  nat >> (fn n => (n, n)))) 

335 
>> (Binder o triple2); 

336 

51654
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

337 
val mixfix_body = mfix  strcture  binder  infxl  infxr  infx; 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

338 

8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

339 
fun annotation guard body = $$$ "("  guard (body  $$$ ")"); 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

340 
fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn; 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

341 

8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

342 
in 
18669  343 

51654
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

344 
val mixfix = annotation !!! mixfix_body; 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

345 
val mixfix' = annotation I mixfix_body; 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

346 
val opt_mixfix = opt_annotation !!! mixfix_body; 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

347 
val opt_mixfix' = opt_annotation I mixfix_body; 
8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

348 

8450b944e58a
just one syntax category "mixfix"  check structure annotation semantically;
wenzelm
parents:
51627
diff
changeset

349 
end; 
5826  350 

351 

18669  352 
(* fixes *) 
5826  353 

21400  354 
val where_ = $$$ "where"; 
355 

42299  356 
val const_decl = name  ($$$ "::"  !!! typ)  opt_mixfix >> triple1; 
30339  357 
val const_binding = binding  ($$$ "::"  !!! typ)  opt_mixfix >> triple1; 
18669  358 

28081
d664b2c1dfe6
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

359 
val params = Scan.repeat1 binding  Scan.option ($$$ "::"  !!! typ) 
18669  360 
>> (fn (xs, T) => map (rpair T) xs); 
361 

362 
val fixes = 

45331
6e0a8aba99ec
more liberal Parse.fixes, to avoid overlap of mixfix with ispattern (notably in 'obtain' syntax);
wenzelm
parents:
44357
diff
changeset

363 
and_list1 (binding  Scan.option ($$$ "::"  typ)  mixfix' >> (single o triple1)  
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
40800
diff
changeset

364 
params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; 
5826  365 

19845  366 
val for_fixes = Scan.optional ($$$ "for"  !!! fixes) []; 
367 

5826  368 

27877  369 
(* embedded source text *) 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27815
diff
changeset

370 

59809  371 
val ML_source = input (group (fn () => "ML source") text); 
372 
val document_source = input (group (fn () => "document source") text); 

27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27815
diff
changeset

373 

631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27815
diff
changeset

374 

5826  375 
(* terms *) 
376 

40793
d21aedaa91e7
added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents:
40296
diff
changeset

377 
val tm = short_ident  long_ident  sym_ident  term_var  number  string; 
5826  378 

44357  379 
val term_group = group (fn () => "term") tm; 
380 
val prop_group = group (fn () => "proposition") tm; 

27753
94b672153b49
sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents:
27737
diff
changeset

381 

94b672153b49
sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents:
27737
diff
changeset

382 
val term = inner_syntax term_group; 
94b672153b49
sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents:
27737
diff
changeset

383 
val prop = inner_syntax prop_group; 
5826  384 

44357  385 
val const = inner_syntax (group (fn () => "constant") xname); 
42300
0d1cbc1fe579
notation: proper markup for type constructor / constant;
wenzelm
parents:
42299
diff
changeset

386 

56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56202
diff
changeset

387 
val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string  cartouche)); 
40793
d21aedaa91e7
added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents:
40296
diff
changeset

388 

5826  389 

6949  390 
(* patterns *) 
6935  391 

6949  392 
val is_terms = Scan.repeat1 ($$$ "is"  term); 
6935  393 
val is_props = Scan.repeat1 ($$$ "is"  prop); 
394 

19585  395 
val propp = prop  Scan.optional ($$$ "("  !!! (is_props  $$$ ")")) []; 
6949  396 
val termp = term  Scan.optional ($$$ "("  !!! (is_terms  $$$ ")")) []; 
6935  397 

398 

22119  399 
(* targets *) 
19811  400 

45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45331
diff
changeset

401 
val target = ($$$ "("  $$$ "in")  !!! (position xname  $$$ ")"); 
22119  402 
val opt_target = Scan.option target; 
12272  403 

56201  404 

405 
(* arguments within outer syntax *) 

406 

407 
local 

408 

409 
val argument_kinds = 

59081  410 
[Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var, 
411 
Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim]; 

56201  412 

413 
fun arguments is_symid = 

414 
let 

415 
fun argument blk = 

416 
group (fn () => "argument") 

417 
(Scan.one (fn tok => 

418 
let val kind = Token.kind_of tok in 

419 
member (op =) argument_kinds kind orelse 

420 
Token.keyword_with is_symid tok orelse 

421 
(blk andalso Token.keyword_with (fn s => s = ",") tok) 

422 
end)); 

423 

424 
fun args blk x = Scan.optional (args1 blk) [] x 

425 
and args1 blk x = 

426 
((Scan.repeat1 

427 
(Scan.repeat1 (argument blk)  

428 
argsp "(" ")"  

429 
argsp "[" "]")) >> flat) x 

430 
and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x; 

431 
in (args, args1) end; 

432 

433 
in 

434 

435 
val args = #1 (arguments Token.ident_or_symbolic) false; 

436 
fun args1 is_symid = #2 (arguments is_symid) false; 

437 

438 
end; 

439 

58028
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

440 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

441 
(* attributes *) 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

442 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

443 
val attrib = position liberal_name  !!! args >> uncurry Token.src; 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

444 
val attribs = $$$ "["  list attrib  $$$ "]"; 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

445 
val opt_attribs = Scan.optional attribs []; 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

446 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

447 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

448 
(* theorem references *) 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

449 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

450 
val thm_sel = $$$ "("  list1 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

451 
(nat  minus  nat >> Facts.FromTo  
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

452 
nat  minus >> Facts.From  
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

453 
nat >> Facts.Single)  $$$ ")"; 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

454 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

455 
val xthm = 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

456 
$$$ "["  attribs  $$$ "]" >> pair (Facts.named "")  
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

457 
(literal_fact >> Facts.Fact  
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

458 
position xname  Scan.option thm_sel >> Facts.Named)  opt_attribs; 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

459 

e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

460 
val xthms1 = Scan.repeat1 xthm; 
e4250d370657
tuned signature  define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset

461 

12272  462 
end; 