author  wenzelm 
Mon, 20 Mar 2017 20:43:26 +0100  
changeset 65335  7634d33c1a79 
parent 64824  330ec9bc4b75 
child 65523  4f2954adc217 
permissions  rwrr 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

1 
/* Title: Pure/Isar/token.scala 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

3 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

4 
Outer token syntax for Isabelle/Isar. 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

5 
*/ 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

6 

d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

7 
package isabelle 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

8 

d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

9 

59083  10 
import scala.collection.mutable 
11 
import scala.util.parsing.input 

12 

13 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

14 
object Token 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

15 
{ 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

16 
/* tokens */ 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

17 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

18 
object Kind extends Enumeration 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

19 
{ 
59081  20 
/*immediate source*/ 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

21 
val COMMAND = Value("command") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

22 
val KEYWORD = Value("keyword") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

23 
val IDENT = Value("identifier") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

24 
val LONG_IDENT = Value("long identifier") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

25 
val SYM_IDENT = Value("symbolic identifier") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

26 
val VAR = Value("schematic variable") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

27 
val TYPE_IDENT = Value("type variable") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

28 
val TYPE_VAR = Value("schematic type variable") 
40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset

29 
val NAT = Value("natural number") 
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset

30 
val FLOAT = Value("floatingpoint number") 
59081  31 
val SPACE = Value("white space") 
32 
/*delimited content*/ 

34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

33 
val STRING = Value("string") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

34 
val ALT_STRING = Value("backquoted string") 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

35 
val VERBATIM = Value("verbatim text") 
55512  36 
val CARTOUCHE = Value("text cartouche") 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

37 
val COMMENT = Value("comment text") 
59081  38 
/*special content*/ 
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

39 
val ERROR = Value("bad input") 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

40 
val UNPARSED = Value("unparsed input") 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

41 
} 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

42 

34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

43 

55494  44 
/* parsers */ 
45 

46 
object Parsers extends Parsers 

47 

48 
trait Parsers extends Scan.Parsers 

49 
{ 

50 
private def delimited_token: Parser[Token] = 

51 
{ 

52 
val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x)) 

53 
val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x)) 

54 
val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) 

55 
val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x)) 

56 
val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x)) 

57 

58 
string  (alt_string  (verb  (cart  cmt))) 

59 
} 

60 

58900  61 
private def other_token(keywords: Keyword.Keywords): Parser[Token] = 
55494  62 
{ 
63 
val letdigs1 = many1(Symbol.is_letdig) 

62103  64 
val sub = one(s => s == Symbol.sub_decoded  s == Symbol.sub) 
55494  65 
val id = 
66 
one(Symbol.is_letter) ~ 

67 
(rep(letdigs1  (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^ 

68 
{ case x ~ y => x + y } 

69 

70 
val nat = many1(Symbol.is_digit) 

71 
val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z } 

72 
val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x } 

73 

74 
val ident = id ~ rep("." ~> id) ^^ 

75 
{ case x ~ Nil => Token(Token.Kind.IDENT, x) 

76 
case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) } 

77 

78 
val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) } 

79 
val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) } 

80 
val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) } 

81 
val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x)) 

82 
val float = 

83 
("" ~ natdot ^^ { case x ~ y => x + y }  natdot) ^^ (x => Token(Token.Kind.FLOAT, x)) 

84 

85 
val sym_ident = 

86 
(many1(Symbol.is_symbolic_char)  one(sym => Symbol.is_symbolic(sym))) ^^ 

87 
(x => Token(Token.Kind.SYM_IDENT, x)) 

88 

58899  89 
val keyword = 
58900  90 
literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x))  
91 
literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x)) 

55494  92 

93 
val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x)) 

94 

95 
val recover_delimited = 

96 
(recover_quoted("\"")  

97 
(recover_quoted("`")  

98 
(recover_verbatim  

99 
(recover_cartouche  recover_comment)))) ^^ (x => Token(Token.Kind.ERROR, x)) 

100 

101 
val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x)) 

102 

103 
space  (recover_delimited  

104 
(((ident  (var_  (type_ident  (type_var  (float  (nat_  sym_ident))))))  

58899  105 
keyword)  bad)) 
55494  106 
} 
107 

58900  108 
def token(keywords: Keyword.Keywords): Parser[Token] = 
109 
delimited_token  other_token(keywords) 

55494  110 

58900  111 
def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context) 
55510
1585a65aad64
tuned signature  emphasize lineoriented aspect;
wenzelm
parents:
55505
diff
changeset

112 
: Parser[(Token, Scan.Line_Context)] = 
55494  113 
{ 
114 
val string = 

55510
1585a65aad64
tuned signature  emphasize lineoriented aspect;
wenzelm
parents:
55505
diff
changeset

115 
quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) } 
55494  116 
val alt_string = 
55510
1585a65aad64
tuned signature  emphasize lineoriented aspect;
wenzelm
parents:
55505
diff
changeset

117 
quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } 
1585a65aad64
tuned signature  emphasize lineoriented aspect;
wenzelm
parents:
55505
diff
changeset

118 
val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } 
1585a65aad64
tuned signature  emphasize lineoriented aspect;
wenzelm
parents:
55505
diff
changeset

119 
val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) } 
1585a65aad64
tuned signature  emphasize lineoriented aspect;
wenzelm
parents:
55505
diff
changeset

120 
val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } 
58900  121 
val other = other_token(keywords) ^^ { case x => (x, Scan.Finished) } 
55494  122 

123 
string  (alt_string  (verb  (cart  (cmt  other)))) 

124 
} 

125 
} 

126 

127 

59083  128 
/* explode */ 
129 

130 
def explode(keywords: Keyword.Keywords, inp: CharSequence): List[Token] = 

64824  131 
Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match { 
59083  132 
case Parsers.Success(tokens, _) => tokens 
133 
case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString) 

134 
} 

135 

136 
def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context) 

137 
: (List[Token], Scan.Line_Context) = 

138 
{ 

64824  139 
var in: input.Reader[Char] = Scan.char_reader(inp) 
59083  140 
val toks = new mutable.ListBuffer[Token] 
141 
var ctxt = context 

142 
while (!in.atEnd) { 

143 
Parsers.parse(Parsers.token_line(keywords, ctxt), in) match { 

60215  144 
case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest 
59083  145 
case Parsers.NoSuccess(_, rest) => 
146 
error("Unexpected failure of tokenizing input:\n" + rest.source.toString) 

147 
} 

148 
} 

149 
(toks.toList, ctxt) 

150 
} 

151 

64671  152 
val newline: Token = explode(Keyword.Keywords.empty, "\n").head 
153 

59083  154 

59735  155 
/* implode */ 
156 

157 
def implode(toks: List[Token]): String = 

158 
toks match { 

159 
case List(tok) => tok.source 

60215  160 
case _ => toks.map(_.source).mkString 
59735  161 
} 
162 

163 

34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

164 
/* token reader */ 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

165 

56464  166 
object Pos 
167 
{ 

59708
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

168 
val none: Pos = new Pos(0, 0, "", "") 
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

169 
val start: Pos = new Pos(1, 1, "", "") 
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

170 
def file(file: String): Pos = new Pos(1, 1, file, "") 
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

171 
def id(id: String): Pos = new Pos(0, 1, "", id) 
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59708
diff
changeset

172 
val command: Pos = id(Markup.COMMAND) 
56464  173 
} 
174 

59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

175 
final class Pos private[Token]( 
59696  176 
val line: Int, 
177 
val offset: Symbol.Offset, 

59708
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

178 
val file: String, 
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

179 
val id: String) 
64824  180 
extends input.Position 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

181 
{ 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

182 
def column = 0 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

183 
def lineContents = "" 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

184 

56464  185 
def advance(token: Token): Pos = 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

186 
{ 
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

187 
var line1 = line 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

188 
var offset1 = offset 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

189 
for (s < Symbol.iterator(token.source)) { 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

190 
if (line1 > 0 && Symbol.is_newline(s)) line1 += 1 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

191 
if (offset1 > 0) offset1 += 1 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

192 
} 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

193 
if (line1 == line && offset1 == offset) this 
59708
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

194 
else new Pos(line1, offset1, file, id) 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

195 
} 
56464  196 

59695  197 
private def position(end_offset: Symbol.Offset): Position.T = 
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

198 
(if (line > 0) Position.Line(line) else Nil) ::: 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

199 
(if (offset > 0) Position.Offset(offset) else Nil) ::: 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

200 
(if (end_offset > 0) Position.End_Offset(end_offset) else Nil) ::: 
59708
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

201 
(if (file != "") Position.File(file) else Nil) ::: 
bf6ca55aae13
proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents:
59707
diff
changeset

202 
(if (id != "") Position.Id_String(id) else Nil) 
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

203 

9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

204 
def position(): Position.T = position(0) 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

205 
def position(token: Token): Position.T = position(advance(token).offset) 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59122
diff
changeset

206 

64728  207 
override def toString: String = Position.here(position(), delimited = false) 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

208 
} 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

209 

64824  210 
abstract class Reader extends input.Reader[Token] 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

211 

56464  212 
private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

213 
{ 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

214 
def first = tokens.head 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

215 
def rest = new Token_Reader(tokens.tail, pos.advance(first)) 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34143
diff
changeset

216 
def atEnd = tokens.isEmpty 
34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

217 
} 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

218 

59707  219 
def reader(tokens: List[Token], start: Token.Pos): Reader = 
220 
new Token_Reader(tokens, start) 

65335  221 

222 

223 
/* XML data representation */ 

224 

225 
val encode: XML.Encode.T[Token] = (tok: Token) => 

226 
{ 

227 
import XML.Encode._ 

228 
pair(int, string)(tok.kind.id, tok.source) 

229 
} 

230 

231 
val decode: XML.Decode.T[Token] = (body: XML.Body) => 

232 
{ 

233 
import XML.Decode._ 

234 
val (k, s) = pair(int, string)(body) 

235 
Token(Kind(k), s) 

236 
} 

34139
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

237 
} 
d1ded303fe0e
Outer lexical syntax for Isabelle/Isar  Scala version.
wenzelm
parents:
diff
changeset

238 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

239 

60215  240 
sealed case class Token(kind: Token.Kind.Value, source: String) 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

241 
{ 
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

242 
def is_command: Boolean = kind == Token.Kind.COMMAND 
63446  243 
def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name 
48718  244 
def is_keyword: Boolean = kind == Token.Kind.KEYWORD 
63446  245 
def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name 
63450  246 
def is_keyword(name: Char): Boolean = 
247 
kind == Token.Kind.KEYWORD && source.length == 1 && source(0) == name 

55505  248 
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) 
48365
d88aefda01c4
basic support for standalone options with external string representation;
wenzelm
parents:
48349
diff
changeset

249 
def is_ident: Boolean = kind == Token.Kind.IDENT 
48605
e777363440d6
allow negative int values as well, according to real = int  float;
wenzelm
parents:
48599
diff
changeset

250 
def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT 
46943  251 
def is_string: Boolean = kind == Token.Kind.STRING 
48349
a78e5d399599
support Session.Queue with ordering and dependencies;
wenzelm
parents:
48335
diff
changeset

252 
def is_nat: Boolean = kind == Token.Kind.NAT 
48365
d88aefda01c4
basic support for standalone options with external string representation;
wenzelm
parents:
48349
diff
changeset

253 
def is_float: Boolean = kind == Token.Kind.FLOAT 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

254 
def is_name: Boolean = 
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

255 
kind == Token.Kind.IDENT  
62969  256 
kind == Token.Kind.LONG_IDENT  
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

257 
kind == Token.Kind.SYM_IDENT  
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

258 
kind == Token.Kind.STRING  
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

259 
kind == Token.Kind.NAT 
64471
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63477
diff
changeset

260 
def is_embedded: Boolean = is_name  
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63477
diff
changeset

261 
kind == Token.Kind.CARTOUCHE  
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63477
diff
changeset

262 
kind == Token.Kind.VAR  
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63477
diff
changeset

263 
kind == Token.Kind.TYPE_IDENT  
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63477
diff
changeset

264 
kind == Token.Kind.TYPE_VAR 
62969  265 
def is_text: Boolean = is_name  kind == Token.Kind.VERBATIM  kind == Token.Kind.CARTOUCHE 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

266 
def is_space: Boolean = kind == Token.Kind.SPACE 
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

267 
def is_comment: Boolean = kind == Token.Kind.COMMENT 
51048
123be08eed88
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
wenzelm
parents:
48754
diff
changeset

268 
def is_improper: Boolean = is_space  is_comment 
48599  269 
def is_proper: Boolean = !is_space && !is_comment 
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

270 
def is_error: Boolean = kind == Token.Kind.ERROR 
47012
0e246130486b
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents:
46943
diff
changeset

271 
def is_unparsed: Boolean = kind == Token.Kind.UNPARSED 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

272 

48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

273 
def is_unfinished: Boolean = is_error && 
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

274 
(source.startsWith("\"")  
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

275 
source.startsWith("`")  
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

276 
source.startsWith("{*")  
57021
6a8fd2ac6756
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
wenzelm
parents:
56998
diff
changeset

277 
source.startsWith("(*")  
6a8fd2ac6756
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
wenzelm
parents:
56998
diff
changeset

278 
source.startsWith(Symbol.open)  
6a8fd2ac6756
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
wenzelm
parents:
56998
diff
changeset

279 
source.startsWith(Symbol.open_decoded)) 
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48718
diff
changeset

280 

63450  281 
def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_)) 
282 
def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_)) 

283 

63446  284 
def is_begin: Boolean = is_keyword("begin") 
285 
def is_end: Boolean = is_command("end") 

63477
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63450
diff
changeset

286 
def is_begin_or_command: Boolean = is_begin  is_command 
43611  287 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

288 
def content: String = 
55492
28d4db6c6e79
tuned signature  separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55137
diff
changeset

289 
if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source) 
28d4db6c6e79
tuned signature  separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55137
diff
changeset

290 
else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source) 
28d4db6c6e79
tuned signature  separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55137
diff
changeset

291 
else if (kind == Token.Kind.VERBATIM) Scan.Parsers.verbatim_content(source) 
28d4db6c6e79
tuned signature  separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55137
diff
changeset

292 
else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source) 
28d4db6c6e79
tuned signature  separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55137
diff
changeset

293 
else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source) 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

294 
else source 
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
34311
diff
changeset

295 
} 