author  wenzelm 
Tue, 31 Jul 2018 21:21:20 +0200  
changeset 68730  0bc491938780 
parent 68729  3a02b424d5fb 
child 69851  29a4f633609e 
permissions  rwrr 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

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

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

4 
Outer token syntax for Isabelle/Isar. 
5825  5 
*) 
6 

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

7 
signature TOKEN = 
5825  8 
sig 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

9 
datatype kind = 
59081  10 
(*immediate source*) 
11 
Command  Keyword  Ident  Long_Ident  Sym_Ident  Var  Type_Ident  Type_Var  Nat  

12 
Float  Space  

13 
(*delimited content*) 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

14 
String  Alt_String  Verbatim  Cartouche  Comment of Comment.kind option  
59081  15 
(*special content*) 
61819  16 
Error of string  EOF 
58012  17 
val str_of_kind: kind > string 
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55750
diff
changeset

18 
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} 
58012  19 
type T 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

20 
type src = T list 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

21 
type name_value = {name: string, kind: string, print: Proof.context > Markup.T * xstring} 
27814  22 
datatype value = 
58012  23 
Source of src  
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

24 
Literal of bool * Markup.T  
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

25 
Name of name_value * morphism  
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

26 
Typ of typ  
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

27 
Term of term  
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
56202
diff
changeset

28 
Fact of string option * thm list  
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

29 
Attribute of morphism > attribute  
58017  30 
Declaration of declaration  
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

31 
Files of file Exn.result list 
55708  32 
val pos_of: T > Position.T 
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset

33 
val range_of: T list > Position.range 
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
67652
diff
changeset

34 
val adjust_offsets: (int > int option) > T > T 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

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

36 
val is_eof: T > bool 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

37 
val not_eof: T > bool 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

38 
val stopper: T Scan.stopper 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

39 
val kind_of: T > kind 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

40 
val is_kind: kind > T > bool 
46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset

41 
val is_command: T > bool 
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59913
diff
changeset

42 
val keyword_with: (string > bool) > T > bool 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59924
diff
changeset

43 
val is_command_modifier: T > bool 
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59913
diff
changeset

44 
val ident_with: (string > bool) > T > bool 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

45 
val is_proper: T > bool 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

46 
val is_comment: T > bool 
67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

47 
val is_informal_comment: T > bool 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

48 
val is_formal_comment: T > bool 
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
68298
diff
changeset

49 
val is_ignored: T > bool 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

50 
val is_begin_ignore: T > bool 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

51 
val is_end_ignore: T > bool 
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset

52 
val is_error: T > bool 
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

53 
val is_space: T > bool 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

54 
val is_blank: T > bool 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

55 
val is_newline: T > bool 
59795  56 
val content_of: T > string 
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

57 
val source_of: T > string 
59809  58 
val input_of: T > Input.source 
59795  59 
val inner_syntax_of: T > string 
56202  60 
val keyword_markup: bool * Markup.T > string > Markup.T 
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

61 
val completion_report: T > Position.report_text list 
59125  62 
val reports: Keyword.keywords > T > Position.report_text list 
63 
val markups: Keyword.keywords > T > Markup.T list 

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

64 
val unparse: T > string 
55745  65 
val print: T > string 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

66 
val text_of: T > string * string 
54520
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset

67 
val get_files: T > file Exn.result list 
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset

68 
val put_files: file Exn.result list > T > T 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

69 
val get_value: T > value option 
61822  70 
val reports_of_value: T > Position.report list 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

71 
val name_value: name_value > value 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

72 
val get_name: T > name_value option 
59646  73 
val declare_maxidx: T > Proof.context > Proof.context 
61820  74 
val map_facts: (string option > thm list > thm list) > T > T 
67652  75 
val trim_context_src: src > src 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

76 
val transform: morphism > T > T 
55914
c5b752d549e3
clarified init_assignable: make doublesure that initial values are reset;
wenzelm
parents:
55828
diff
changeset

77 
val init_assignable: T > T 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

78 
val assign: value option > T > T 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

79 
val evaluate: ('a > value) > (T > 'a) > T > 'a 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
32738
diff
changeset

80 
val closure: T > T 
58012  81 
val pretty_value: Proof.context > T > Pretty.T 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

82 
val name_of_src: src > string * Position.T 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

83 
val args_of_src: src > T list 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

84 
val checked_src: src > bool 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

85 
val check_src: Proof.context > (Proof.context > 'a Name_Space.table) > src > src * 'a 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

86 
val pretty_src: Proof.context > src > Pretty.T 
27814  87 
val ident_or_symbolic: string > bool 
61471  88 
val read_cartouche: Symbol_Pos.T list > T 
67497  89 
val tokenize: Keyword.keywords > {strict: bool} > Symbol_Pos.T list > T list 
59083  90 
val explode: Keyword.keywords > Position.T > string > T list 
67495  91 
val explode0: Keyword.keywords > string > T list 
63640  92 
val print_name: Keyword.keywords > string > string 
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

93 
val make: (int * int) * string > Position.T > T * Position.T 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

94 
val make_string: string * Position.T > T 
63019  95 
val make_int: int > T list 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

96 
val make_src: string * Position.T > T list > src 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

97 
type 'a parser = T list > 'a * T list 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

98 
type 'a context_parser = Context.generic * T list > 'a * (Context.generic * T list) 
67504  99 
val read_body: Keyword.keywords > 'a parser > Symbol_Pos.T list > 'a option 
58903  100 
val read_antiq: Keyword.keywords > 'a parser > Symbol_Pos.T list * Position.T > 'a 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

101 
val syntax_generic: 'a context_parser > src > Context.generic > 'a * Context.generic 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

102 
val syntax: 'a context_parser > src > Proof.context > 'a * Proof.context 
5825  103 
end; 
104 

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

105 
structure Token: TOKEN = 
5825  106 
struct 
107 

108 
(** tokens **) 

109 

58012  110 
(* token kind *) 
5825  111 

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

112 
datatype kind = 
59081  113 
(*immediate source*) 
114 
Command  Keyword  Ident  Long_Ident  Sym_Ident  Var  Type_Ident  Type_Var  Nat  

115 
Float  Space  

116 
(*delimited content*) 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

117 
String  Alt_String  Verbatim  Cartouche  Comment of Comment.kind option  
59081  118 
(*special content*) 
61819  119 
Error of string  EOF; 
5825  120 

121 
val str_of_kind = 

7026  122 
fn Command => "command" 
123 
 Keyword => "keyword" 

5825  124 
 Ident => "identifier" 
59081  125 
 Long_Ident => "long identifier" 
126 
 Sym_Ident => "symbolic identifier" 

5825  127 
 Var => "schematic variable" 
59081  128 
 Type_Ident => "type variable" 
129 
 Type_Var => "schematic type variable" 

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

130 
 Nat => "natural number" 
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38229
diff
changeset

131 
 Float => "floatingpoint number" 
59081  132 
 Space => "white space" 
55103  133 
 String => "quoted string" 
59081  134 
 Alt_String => "backquoted string" 
5825  135 
 Verbatim => "verbatim text" 
55103  136 
 Cartouche => "text cartouche" 
67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

137 
 Comment NONE => "informal comment" 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

138 
 Comment (SOME _) => "formal comment" 
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset

139 
 Error _ => "bad input" 
48911
5debc3e4fa81
tuned messages: endofinput rarely means physical endoffile from the past;
wenzelm
parents:
48905
diff
changeset

140 
 EOF => "endofinput"; 
5825  141 

59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

142 
val immediate_kinds = 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

143 
Vector.fromList 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

144 
[Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space]; 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

145 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

146 
val delimited_kind = 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

147 
(fn String => true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

148 
 Alt_String => true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

149 
 Verbatim => true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

150 
 Cartouche => true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

151 
 Comment _ => true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

152 
 _ => false); 
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset

153 

5825  154 

58012  155 
(* datatype token *) 
156 

157 
(*The value slot assigns an (optional) internal value to a token, 

158 
usually as a sideeffect of special scanner setup (see also 

159 
args.ML). Note that an assignable ref designates an intermediate 

160 
state of internalization  it is NOT meant to persist.*) 

161 

162 
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; 

163 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

164 
type name_value = {name: string, kind: string, print: Proof.context > Markup.T * xstring}; 
58012  165 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

166 
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot 
58012  167 

168 
and slot = 

169 
Slot  

170 
Value of value option  

171 
Assignable of value option Unsynchronized.ref 

172 

173 
and value = 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

174 
Source of T list  
58012  175 
Literal of bool * Markup.T  
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

176 
Name of name_value * morphism  
58012  177 
Typ of typ  
178 
Term of term  

179 
Fact of string option * thm list  (*optional name for dynamic fact, i.e. fact "variable"*) 

180 
Attribute of morphism > attribute  

58017  181 
Declaration of declaration  
58012  182 
Files of file Exn.result list; 
183 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

184 
type src = T list; 
58012  185 

186 

27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

187 
(* position *) 
5825  188 

55708  189 
fun pos_of (Token ((_, (pos, _)), _, _)) = pos; 
190 
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; 

27663  191 

55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset

192 
fun range_of (toks as tok :: _) = 
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset

193 
let val pos' = end_pos_of (List.last toks) 
62797  194 
in Position.range (pos_of tok, pos') end 
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset

195 
 range_of [] = Position.no_range; 
5825  196 

68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
67652
diff
changeset

197 
fun adjust_offsets adjust (Token ((x, range), y, z)) = 
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
67652
diff
changeset

198 
Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z); 
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
67652
diff
changeset

199 

5825  200 

58855  201 
(* stopper *) 
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

202 

27814  203 
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); 
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

204 
val eof = mk_eof Position.none; 
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

205 

27814  206 
fun is_eof (Token (_, (EOF, _), _)) = true 
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

207 
 is_eof _ = false; 
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

208 

d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

209 
val not_eof = not o is_eof; 
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

210 

27752
ea7d573e565f
removed obsolete range_of (already included in position);
wenzelm
parents:
27747
diff
changeset

211 
val stopper = 
55708  212 
Scan.stopper (fn [] => eof  toks => mk_eof (end_pos_of (List.last toks))) is_eof; 
27733
d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

213 

d3d7038fb7b5
abstract type Scan.stopper, position taken from last input token;
wenzelm
parents:
27663
diff
changeset

214 

5825  215 
(* kind of token *) 
216 

27814  217 
fun kind_of (Token (_, (k, _), _)) = k; 
218 
fun is_kind k (Token (_, (k', _), _)) = k = k'; 

5825  219 

46811
03a2dc9e0624
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents:
45666
diff
changeset

220 
val is_command = is_kind Command; 
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59112
diff
changeset

221 

27814  222 
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x 
7026  223 
 keyword_with _ _ = false; 
5825  224 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

225 
val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified"); 
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59913
diff
changeset

226 

27814  227 
fun ident_with pred (Token (_, (Ident, x), _)) = pred x 
16029  228 
 ident_with _ _ = false; 
229 

68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
68298
diff
changeset

230 
fun is_ignored (Token (_, (Space, _), _)) = true 
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
68298
diff
changeset

231 
 is_ignored (Token (_, (Comment NONE, _), _)) = true 
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
68298
diff
changeset

232 
 is_ignored _ = false; 
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
68298
diff
changeset

233 

27814  234 
fun is_proper (Token (_, (Space, _), _)) = false 
67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

235 
 is_proper (Token (_, (Comment _, _), _)) = false 
5825  236 
 is_proper _ = true; 
237 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

238 
fun is_comment (Token (_, (Comment _, _), _)) = true 
17069  239 
 is_comment _ = false; 
240 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

241 
fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

242 
 is_informal_comment _ = false; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

243 

78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

244 
fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

245 
 is_formal_comment _ = false; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

246 

78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

247 
fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true 
8580  248 
 is_begin_ignore _ = false; 
249 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

250 
fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true 
8580  251 
 is_end_ignore _ = false; 
252 

48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset

253 
fun is_error (Token (_, (Error _, _), _)) = true 
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset

254 
 is_error _ = false; 
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48743
diff
changeset

255 

8651  256 

17069  257 
(* blanks and newlines  space tokens obey lines *) 
8651  258 

48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

259 
fun is_space (Token (_, (Space, _), _)) = true 
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

260 
 is_space _ = false; 
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

261 

27814  262 
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) 
17069  263 
 is_blank _ = false; 
264 

27814  265 
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x 
8651  266 
 is_newline _ = false; 
267 

5825  268 

14991  269 
(* token content *) 
9155  270 

59795  271 
fun content_of (Token (_, (_, x), _)) = x; 
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

272 
fun source_of (Token ((source, _), _, _)) = source; 
25642
ebdff0dca2a5
text_of: made even more robust against recurrent errors;
wenzelm
parents:
25582
diff
changeset

273 

59809  274 
fun input_of (Token ((source, range), (kind, _), _)) = 
59064  275 
Input.source (delimited_kind kind) source range; 
27873  276 

59795  277 
fun inner_syntax_of tok = 
278 
let val x = content_of tok 

59809  279 
in if YXML.detect x then x else Syntax.implode_input (input_of tok) end; 
27747
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset

280 

d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset

281 

55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

282 
(* markup reports *) 
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

283 

4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

284 
local 
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

285 

4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

286 
val token_kind_markup = 
59124  287 
fn Var => (Markup.var, "") 
59081  288 
 Type_Ident => (Markup.tfree, "") 
289 
 Type_Var => (Markup.tvar, "") 

290 
 String => (Markup.string, "") 

291 
 Alt_String => (Markup.alt_string, "") 

292 
 Verbatim => (Markup.verbatim, "") 

293 
 Cartouche => (Markup.cartouche, "") 

67440  294 
 Comment _ => (Markup.comment, "") 
64677
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
64421
diff
changeset

295 
 Error msg => (Markup.bad (), msg) 
59124  296 
 _ => (Markup.empty, ""); 
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

297 

59125  298 
fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), "")); 
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59112
diff
changeset

299 

59125  300 
fun command_markups keywords x = 
66067  301 
if Keyword.is_theory_end keywords x then [Markup.keyword2 > Markup.keyword_properties] 
65174
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
64677
diff
changeset

302 
else 
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
64677
diff
changeset

303 
(if Keyword.is_proof_asm keywords x then [Markup.keyword3] 
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
64677
diff
changeset

304 
else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] 
c0388fbd8096
avoid extra decorations for regular command keywords;
wenzelm
parents:
64677
diff
changeset

305 
else [Markup.keyword1]) 
66066  306 
> map Markup.command_properties; 
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59112
diff
changeset

307 

56063  308 
in 
309 

56202  310 
fun keyword_markup (important, keyword) x = 
311 
if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; 

55919
2eb8c13339a5
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents:
55916
diff
changeset

312 

55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

313 
fun completion_report tok = 
55914
c5b752d549e3
clarified init_assignable: make doublesure that initial values are reset;
wenzelm
parents:
55828
diff
changeset

314 
if is_kind Keyword tok 
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

315 
then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) 
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

316 
else []; 
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

317 

59125  318 
fun reports keywords tok = 
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59112
diff
changeset

319 
if is_command tok then 
59125  320 
keyword_reports tok (command_markups keywords (content_of tok)) 
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59112
diff
changeset

321 
else if is_kind Keyword tok then 
66044  322 
keyword_reports tok 
66067  323 
[keyword_markup (false, Markup.keyword2 > Markup.keyword_properties) (content_of tok)] 
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

324 
else 
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

325 
let 
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

326 
val pos = pos_of tok; 
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

327 
val (m, text) = token_kind_markup (kind_of tok); 
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

328 
val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos)); 
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68183
diff
changeset

329 
in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end; 
55915
607948c90bf0
suppress short abbreviations more uniformly, for outer and quasiouter syntax;
wenzelm
parents:
55914
diff
changeset

330 

59125  331 
fun markups keywords = map (#2 o #1) o reports keywords; 
55914
c5b752d549e3
clarified init_assignable: make doublesure that initial values are reset;
wenzelm
parents:
55828
diff
changeset

332 

55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

333 
end; 
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

334 

4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55709
diff
changeset

335 

27747
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset

336 
(* unparse *) 
d41abb7bc08a
token: maintain of source, which retains original position information;
wenzelm
parents:
27733
diff
changeset

337 

27814  338 
fun unparse (Token (_, (kind, x), _)) = 
14991  339 
(case kind of 
43773  340 
String => Symbol_Pos.quote_string_qq x 
59081  341 
 Alt_String => Symbol_Pos.quote_string_bq x 
43773  342 
 Verbatim => enclose "{*" "*}" x 
55033  343 
 Cartouche => cartouche x 
67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

344 
 Comment NONE => enclose "(*" "*)" x 
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset

345 
 EOF => "" 
14991  346 
 _ => x); 
347 

59125  348 
fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); 
55745  349 

23788
54ce229dc858
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents:
23729
diff
changeset

350 
fun text_of tok = 
58861
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

351 
let 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

352 
val k = str_of_kind (kind_of tok); 
59125  353 
val ms = markups Keyword.empty_keywords tok; 
58861
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

354 
val s = unparse tok; 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

355 
in 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

356 
if s = "" then (k, "") 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

357 
else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) 
59125  358 
then (k ^ " " ^ Markup.markups ms s, "") 
359 
else (k, Markup.markups ms s) 

58861
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58855
diff
changeset

360 
end; 
23729
d1ba656978c5
separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents:
23721
diff
changeset

361 

5825  362 

363 

27814  364 
(** associated values **) 
365 

48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset

366 
(* inlined file content *) 
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset

367 

54519
5fed81762406
maintain blobs within document state: digest + text in ML, digestonly in Scala;
wenzelm
parents:
51266
diff
changeset

368 
fun get_files (Token (_, _, Value (SOME (Files files)))) = files 
5fed81762406
maintain blobs within document state: digest + text in ML, digestonly in Scala;
wenzelm
parents:
51266
diff
changeset

369 
 get_files _ = []; 
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset

370 

54519
5fed81762406
maintain blobs within document state: digest + text in ML, digestonly in Scala;
wenzelm
parents:
51266
diff
changeset

371 
fun put_files [] tok = tok 
5fed81762406
maintain blobs within document state: digest + text in ML, digestonly in Scala;
wenzelm
parents:
51266
diff
changeset

372 
 put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) 
55708  373 
 put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); 
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset

374 

e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48771
diff
changeset

375 

27814  376 
(* access values *) 
377 

378 
fun get_value (Token (_, _, Value v)) = v 

379 
 get_value _ = NONE; 

380 

381 
fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) 

382 
 map_value _ tok = tok; 

383 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

384 

61822  385 
(* reports of value *) 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

386 

61822  387 
fun get_assignable_value (Token (_, _, Assignable r)) = ! r 
388 
 get_assignable_value (Token (_, _, Value v)) = v 

389 
 get_assignable_value _ = NONE; 

60211  390 

55914
c5b752d549e3
clarified init_assignable: make doublesure that initial values are reset;
wenzelm
parents:
55828
diff
changeset

391 
fun reports_of_value tok = 
60211  392 
(case get_assignable_value tok of 
56063  393 
SOME (Literal markup) => 
394 
let 

395 
val pos = pos_of tok; 

396 
val x = content_of tok; 

397 
in 

398 
if Position.is_reported pos then 

399 
map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) 

400 
else [] 

401 
end 

402 
 _ => []); 

55914
c5b752d549e3
clarified init_assignable: make doublesure that initial values are reset;
wenzelm
parents:
55828
diff
changeset

403 

27814  404 

61822  405 
(* name value *) 
406 

407 
fun name_value a = Name (a, Morphism.identity); 

408 

409 
fun get_name tok = 

410 
(case get_assignable_value tok of 

411 
SOME (Name (a, _)) => SOME a 

412 
 _ => NONE); 

413 

414 

59646  415 
(* maxidx *) 
416 

417 
fun declare_maxidx tok = 

418 
(case get_value tok of 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

419 
SOME (Source src) => fold declare_maxidx src 
59646  420 
 SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T) 
421 
 SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t) 

422 
 SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths 

423 
 SOME (Attribute _) => I (* FIXME !? *) 

424 
 SOME (Declaration decl) => 

425 
(fn ctxt => 

426 
let val ctxt' = Context.proof_map (Morphism.form decl) ctxt 

427 
in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end) 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

428 
 _ => I); 
59646  429 

430 

61080  431 
(* fact values *) 
432 

433 
fun map_facts f = 

434 
map_value (fn v => 

435 
(case v of 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

436 
Source src => Source (map (map_facts f) src) 
61820  437 
 Fact (a, ths) => Fact (a, f a ths) 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

438 
 _ => v)); 
61080  439 

67652  440 
val trim_context_src = (map o map_facts) (K (map Thm.trim_context)); 
441 

61080  442 

58012  443 
(* transform *) 
444 

445 
fun transform phi = 

446 
map_value (fn v => 

447 
(case v of 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

448 
Source src => Source (map (transform phi) src) 
58012  449 
 Literal _ => v 
450 
 Name (a, psi) => Name (a, psi $> phi) 

451 
 Typ T => Typ (Morphism.typ phi T) 

452 
 Term t => Term (Morphism.term phi t) 

453 
 Fact (a, ths) => Fact (a, Morphism.fact phi ths) 

454 
 Attribute att => Attribute (Morphism.transform phi att) 

58017  455 
 Declaration decl => Declaration (Morphism.transform phi decl) 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

456 
 Files _ => v)); 
58012  457 

458 

459 
(* static binding *) 

460 

461 
(*1st stage: initialize assignable slots*) 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

462 
fun init_assignable tok = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

463 
(case tok of 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

464 
Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE)) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

465 
 Token (_, _, Value _) => tok 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

466 
 Token (_, _, Assignable r) => (r := NONE; tok)); 
58012  467 

468 
(*2nd stage: assign values as sideeffect of scanning*) 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

469 
fun assign v tok = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

470 
(case tok of 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

471 
Token (x, y, Slot) => Token (x, y, Value v) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

472 
 Token (_, _, Value _) => tok 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

473 
 Token (_, _, Assignable r) => (r := v; tok)); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

474 

1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

475 
fun evaluate mk eval arg = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

476 
let val x = eval arg in (assign (SOME (mk x)) arg; x) end; 
58012  477 

478 
(*3rd stage: static closure of final values*) 

479 
fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) 

480 
 closure tok = tok; 

481 

482 

483 
(* pretty *) 

57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

484 

fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

485 
fun pretty_value ctxt tok = 
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

486 
(case get_value tok of 
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

487 
SOME (Literal markup) => 
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

488 
let val x = content_of tok 
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

489 
in Pretty.mark_str (keyword_markup markup x, x) end 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

490 
 SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt)) 
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

491 
 SOME (Typ T) => Syntax.pretty_typ ctxt T 
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

492 
 SOME (Term t) => Syntax.pretty_term ctxt t 
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

493 
 SOME (Fact (_, ths)) => 
62094  494 
Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) 
59125  495 
 _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); 
57944
fff8d328da56
more informative Token.Name with history of morphisms;
wenzelm
parents:
57942
diff
changeset

496 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

497 

1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

498 
(* src *) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

499 

61825  500 
fun dest_src ([]: src) = raise Fail "Empty token source" 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

501 
 dest_src (head :: args) = (head, args); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

502 

1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

503 
fun name_of_src src = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

504 
let 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

505 
val head = #1 (dest_src src); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

506 
val name = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

507 
(case get_name head of 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

508 
SOME {name, ...} => name 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

509 
 NONE => content_of head); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

510 
in (name, pos_of head) end; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

511 

1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

512 
val args_of_src = #2 o dest_src; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

513 

58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

514 
fun pretty_src ctxt src = 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

515 
let 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

516 
val (head, args) = dest_src src; 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

517 
val prt_name = 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

518 
(case get_name head of 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

519 
SOME {print, ...} => Pretty.mark_str (print ctxt) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

520 
 NONE => Pretty.str (content_of head)); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

521 
in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

522 

1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

523 
fun checked_src (head :: _) = is_some (get_name head) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

524 
 checked_src [] = true; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

525 

1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

526 
fun check_src ctxt get_table src = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

527 
let 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

528 
val (head, args) = dest_src src; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

529 
val table = get_table ctxt; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

530 
in 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

531 
(case get_name head of 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

532 
SOME {name, ...} => (src, Name_Space.get table name) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

533 
 NONE => 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

534 
let 
64421
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

535 
val pos = pos_of head; 
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

536 
val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos); 
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

537 
val _ = Context_Position.report ctxt pos Markup.operator; 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

538 
val kind = Name_Space.kind_of (Name_Space.space_of_table table); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

539 
fun print ctxt' = 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

540 
Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

541 
val value = name_value {name = name, kind = kind, print = print}; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

542 
val head' = closure (assign (SOME value) head); 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

543 
in (head' :: args, x) end) 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

544 
end; 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

545 

bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

546 

59125  547 

5825  548 
(** scanners **) 
549 

30573  550 
open Basic_Symbol_Pos; 
5825  551 

48764  552 
val err_prefix = "Outer lexical error: "; 
553 

554 
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); 

5825  555 

556 

557 
(* scan symbolic idents *) 

558 

8231  559 
val scan_symid = 
55033  560 
Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol)  
40525
14a2e686bdac
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents:
40523
diff
changeset

561 
Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; 
5825  562 

8231  563 
fun is_symid str = 
564 
(case try Symbol.explode str of 

55033  565 
SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s 
566 
 SOME ss => forall Symbol.is_symbolic_char ss 

8231  567 
 _ => false); 
568 

27814  569 
fun ident_or_symbolic "begin" = false 
570 
 ident_or_symbolic ":" = true 

571 
 ident_or_symbolic "::" = true 

50239  572 
 ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; 
5825  573 

574 

575 
(* scan verbatim text *) 

576 

577 
val scan_verb = 

55107  578 
$$$ "*"  Scan.ahead (~$$ "}")  
58854  579 
Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single; 
5825  580 

581 
val scan_verbatim = 

55107  582 
Scan.ahead ($$ "{"  $$ "*")  
55106  583 
!!! "unclosed verbatim text" 
55107  584 
((Symbol_Pos.scan_pos  $$ "{"  $$ "*")  
61476  585 
(Scan.repeats scan_verb  ($$ "*"  $$ "}"  Symbol_Pos.scan_pos))); 
5825  586 

48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset

587 
val recover_verbatim = 
61476  588 
$$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb; 
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset

589 

5825  590 

55033  591 
(* scan cartouche *) 
592 

593 
val scan_cartouche = 

55104
8284c0d5bf52
clarified scan_cartouche_depth, according to Scala version;
wenzelm
parents:
55103
diff
changeset

594 
Symbol_Pos.scan_pos  
55105  595 
((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content)  Symbol_Pos.scan_pos); 
55033  596 

597 

5825  598 
(* scan space *) 
599 

48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

600 
fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; 
5825  601 

602 
val scan_space = 

48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

603 
Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") []  
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48764
diff
changeset

604 
Scan.many space_symbol @@@ $$$ "\n"; 
5825  605 

606 

27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset

607 
(* scan comment *) 
5825  608 

609 
val scan_comment = 

55105  610 
Symbol_Pos.scan_pos  (Symbol_Pos.scan_comment_body err_prefix  Symbol_Pos.scan_pos); 
5825  611 

612 

27663  613 

27769  614 
(** token sources **) 
5825  615 

23678  616 
local 
617 

27769  618 
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; 
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset

619 

27799  620 
fun token k ss = 
43709
717e96cf9527
discontinued special treatment of hard tabulators;
wenzelm
parents:
42503
diff
changeset

621 
Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); 
27799  622 

623 
fun token_range k (pos1, (ss, pos2)) = 

59112  624 
Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); 
23678  625 

59083  626 
fun scan_token keywords = !!! "bad input" 
48764  627 
(Symbol_Pos.scan_string_qq err_prefix >> token_range String  
59081  628 
Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String  
27799  629 
scan_verbatim >> token_range Verbatim  
55033  630 
scan_cartouche >> token_range Cartouche  
67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
66067
diff
changeset

631 
scan_comment >> token_range (Comment NONE)  
67446  632 
Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss)  
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset

633 
scan_space >> token Space  
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset

634 
(Scan.max token_leq 
27769  635 
(Scan.max token_leq 
58903  636 
(Scan.literal (Keyword.major_keywords keywords) >> pair Command) 
637 
(Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) 

59081  638 
(Lexicon.scan_longid >> pair Long_Ident  
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset

639 
Lexicon.scan_id >> pair Ident  
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40958
diff
changeset

640 
Lexicon.scan_var >> pair Var  
59081  641 
Lexicon.scan_tid >> pair Type_Ident  
642 
Lexicon.scan_tvar >> pair Type_Var  

62782  643 
Symbol_Pos.scan_float >> pair Float  
644 
Symbol_Pos.scan_nat >> pair Nat  

59081  645 
scan_symid >> pair Sym_Ident) >> uncurry token)); 
27769  646 

647 
fun recover msg = 

48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset

648 
(Symbol_Pos.recover_string_qq  
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset

649 
Symbol_Pos.recover_string_bq  
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset

650 
recover_verbatim  
55033  651 
Symbol_Pos.recover_cartouche  
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48741
diff
changeset

652 
Symbol_Pos.recover_comment  
58854  653 
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) 
27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset

654 
>> (single o token (Error msg)); 
23678  655 

656 
in 

5825  657 

67497  658 
fun make_source keywords {strict} = 
58864  659 
let 
59083  660 
val scan_strict = Scan.bulk (scan_token keywords); 
58864  661 
val scan = if strict then scan_strict else Scan.recover scan_strict recover; 
662 
in Source.source Symbol_Pos.stopper scan end; 

27780
7d0910f662f7
more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents:
27769
diff
changeset

663 

61471  664 
fun read_cartouche syms = 
665 
(case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of 

666 
SOME tok => tok 

667 
 NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); 

668 

23678  669 
end; 
5825  670 

30586
9674f64a0702
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents:
30573
diff
changeset

671 

59083  672 
(* explode *) 
673 

67497  674 
fun tokenize keywords strict syms = 
675 
Source.of_list syms > make_source keywords strict > Source.exhaust; 

67495  676 

677 
fun explode keywords pos text = 

67497  678 
Symbol_Pos.explode (text, pos) > tokenize keywords {strict = false}; 
67495  679 

680 
fun explode0 keywords = explode keywords Position.none; 

59083  681 

682 

63640  683 
(* print name in parsable form *) 
684 

685 
fun print_name keywords name = 

686 
((case explode keywords Position.none name of 

687 
[tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) 

688 
 _ => true) ? Symbol_Pos.quote_string_qq) name; 

689 

690 

59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

691 
(* make *) 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

692 

08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

693 
fun make ((k, n), s) pos = 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

694 
let 
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
67652
diff
changeset

695 
val pos' = Position.advance_offsets n pos; 
62797  696 
val range = Position.range (pos, pos'); 
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

697 
val tok = 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

698 
if 0 <= k andalso k < Vector.length immediate_kinds then 
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

699 
Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot) 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

700 
else 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

701 
(case explode Keyword.empty_keywords pos s of 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

702 
[tok] => tok 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

703 
 _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot)) 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

704 
in (tok, pos') end; 
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

705 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

706 
fun make_string (s, pos) = 
62799  707 
let 
708 
val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); 

62800  709 
val pos' = Position.no_range_position pos; 
62799  710 
in Token ((x, (pos', pos')), y, z) end; 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

711 

63019  712 
val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; 
713 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

714 
fun make_src a args = make_string a :: args; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

715 

59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
59083
diff
changeset

716 

58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

717 

bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

718 
(** parsers **) 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

719 

bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

720 
type 'a parser = T list > 'a * T list; 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

721 
type 'a context_parser = Context.generic * T list > 'a * (Context.generic * T list); 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

722 

58045  723 

67502  724 
(* read body  e.g. antiquotation source *) 
58045  725 

67502  726 
fun read_body keywords scan = 
727 
tokenize (Keyword.no_command_keywords keywords) {strict = true} 

728 
#> filter is_proper 

67504  729 
#> Scan.read stopper scan; 
58045  730 

58903  731 
fun read_antiq keywords scan (syms, pos) = 
67502  732 
(case read_body keywords scan syms of 
67504  733 
SOME x => x 
734 
 NONE => error ("Malformed antiquotation" ^ Position.here pos)); 

58045  735 

736 

737 
(* wrapped syntax *) 

738 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

739 
fun syntax_generic scan src context = 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

740 
let 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

741 
val (name, pos) = name_of_src src; 
64421
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

742 
val old_reports = maps reports_of_value src; 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

743 
val args1 = map init_assignable (args_of_src src); 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

744 
fun reported_text () = 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

745 
if Context_Position.is_visible_generic context then 
64421
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

746 
let val new_reports = maps (reports_of_value o closure) args1 in 
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

747 
if old_reports <> new_reports then 
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

748 
map (fn (p, m) => Position.reported_text p m "") new_reports 
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

749 
else [] 
681fae6b00b5
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents:
63936
diff
changeset

750 
end 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

751 
else []; 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

752 
in 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

753 
(case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

754 
(SOME x, (context', [])) => 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

755 
let val _ = Output.report (reported_text ()) 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

756 
in (x, context') end 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

757 
 (_, (context', args2)) => 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

758 
let 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

759 
val print_name = 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

760 
(case get_name (hd src) of 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

761 
NONE => quote name 
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

762 
 SOME {kind, print, ...} => 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

763 
let 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

764 
val ctxt' = Context.proof_of context'; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

765 
val (markup, xname) = print ctxt'; 
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61614
diff
changeset

766 
in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end); 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

767 
val print_args = 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

768 
if null args2 then "" else ":\n " ^ space_implode " " (map print args2); 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

769 
in 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

770 
error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

771 
Markup.markup_report (implode (reported_text ()))) 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

772 
end) 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

773 
end; 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

774 

bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

775 
fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

776 

5825  777 
end; 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

778 

bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

779 
type 'a parser = 'a Token.parser; 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57944
diff
changeset

780 
type 'a context_parser = 'a Token.context_parser; 