--- a/src/Pure/General/antiquote.ML Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/General/antiquote.ML Sun Feb 16 17:50:13 2014 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/General/antiquote.ML
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
-Text with antiquotations of inner items (types, terms, theorems etc.).
+Antiquotations within plain text.
*)
signature ANTIQUOTE =
@@ -13,7 +13,7 @@
val reports_of: ('a -> Position.report_text list) ->
'a antiquote list -> Position.report_text list
val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
- val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
+ val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
end;
@@ -45,10 +45,10 @@
val err_prefix = "Antiquotation lexical error: ";
val scan_txt =
- $$$ "@" --| Scan.ahead (~$$ "{") ||
- Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
+ Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
+ Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
-val scan_ant =
+val scan_antiq_body =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
@@ -58,10 +58,10 @@
val scan_antiq =
Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
- (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
+ (Scan.repeat scan_antiq_body -- ($$ "}" |-- Symbol_Pos.scan_pos)))
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
-val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
+val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text;
end;
@@ -69,7 +69,7 @@
(* read *)
fun read (syms, pos) =
- (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/antiquote.scala Sun Feb 16 17:50:13 2014 +0100
@@ -0,0 +1,55 @@
+/* Title: Pure/ML/antiquote.scala
+ Author: Makarius
+
+Antiquotations within plain text.
+*/
+
+package isabelle
+
+
+import scala.util.parsing.input.CharSequenceReader
+
+
+object Antiquote
+{
+ sealed abstract class Antiquote
+ case class Text(source: String) extends Antiquote
+ case class Antiq(source: String) extends Antiquote
+
+
+ /* parsers */
+
+ object Parsers extends Parsers
+
+ trait Parsers extends Scan.Parsers
+ {
+ private val txt: Parser[String] =
+ rep1("@" ~ guard(one(s => s != "{")) | many1(s => s != "@")) ^^ (x => x.mkString)
+
+ val antiq_other: Parser[String] =
+ many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
+
+ private val antiq_body: Parser[String] =
+ quoted("\"") | (quoted("`") | (cartouche | antiq_other))
+
+ val antiq: Parser[String] =
+ "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
+
+ val antiquote: Parser[Antiquote] =
+ antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x))
+ }
+
+
+ /* read */
+
+ def read(input: CharSequence): List[Antiquote] =
+ {
+ Parsers.parseAll(Parsers.rep(Parsers.antiquote), new CharSequenceReader(input)) match {
+ case Parsers.Success(xs, _) => xs
+ case Parsers.NoSuccess(_, next) =>
+ error("Malformed quotation/antiquotation source" +
+ Position.here(Position.Line(next.pos.line)))
+ }
+ }
+}
+
--- a/src/Pure/General/scan.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/General/scan.scala Sun Feb 16 17:50:13 2014 +0100
@@ -17,14 +17,14 @@
object Scan
{
- /** context of partial scans (line boundary) **/
+ /** context of partial line-oriented scans **/
- abstract class Context
- case object Finished extends Context
- case class Quoted(quote: String) extends Context
- case object Verbatim extends Context
- case class Cartouche(depth: Int) extends Context
- case class Comment(depth: Int) extends Context
+ abstract class Line_Context
+ case object Finished extends Line_Context
+ case class Quoted(quote: String) extends Line_Context
+ case object Verbatim extends Line_Context
+ case class Cartouche(depth: Int) extends Line_Context
+ case class Comment(depth: Int) extends Line_Context
@@ -110,7 +110,7 @@
else body
}
- def quoted_context(quote: Symbol.Symbol, ctxt: Context): Parser[(String, Context)] =
+ def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] =
{
ctxt match {
case Finished =>
@@ -123,7 +123,7 @@
case x ~ None => (x, ctxt) }
case _ => failure("")
}
- }.named("quoted_context")
+ }.named("quoted_line")
def recover_quoted(quote: Symbol.Symbol): Parser[String] =
quote ~ quoted_body(quote) ^^ { case x ~ y => x + y }
@@ -145,7 +145,7 @@
source.substring(2, source.length - 2)
}
- def verbatim_context(ctxt: Context): Parser[(String, Context)] =
+ def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
{
ctxt match {
case Finished =>
@@ -158,7 +158,7 @@
case x ~ None => (x, Verbatim) }
case _ => failure("")
}
- }.named("verbatim_context")
+ }.named("verbatim_line")
val recover_verbatim: Parser[String] =
"{*" ~ verbatim_body ^^ { case x ~ y => x + y }
@@ -194,7 +194,7 @@
def cartouche: Parser[String] =
cartouche_depth(0) ^? { case (x, d) if d == 0 => x }
- def cartouche_context(ctxt: Context): Parser[(String, Context)] =
+ def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
{
val depth =
ctxt match {
@@ -258,7 +258,7 @@
def comment: Parser[String] =
comment_depth(0) ^? { case (x, d) if d == 0 => x }
- def comment_context(ctxt: Context): Parser[(String, Context)] =
+ def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
{
val depth =
ctxt match {
--- a/src/Pure/Isar/outer_syntax.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sun Feb 16 17:50:13 2014 +0100
@@ -137,13 +137,13 @@
def scan(input: CharSequence): List[Token] =
scan(new CharSequenceReader(input))
- def scan_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) =
+ def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
{
var in: Reader[Char] = new CharSequenceReader(input)
val toks = new mutable.ListBuffer[Token]
var ctxt = context
while (!in.atEnd) {
- Token.Parsers.parse(Token.Parsers.token_context(lexicon, is_command, ctxt), in) match {
+ Token.Parsers.parse(Token.Parsers.token_line(lexicon, is_command, ctxt), in) match {
case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
case Token.Parsers.NoSuccess(_, rest) =>
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
--- a/src/Pure/Isar/token.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/Isar/token.scala Sun Feb 16 17:50:13 2014 +0100
@@ -26,7 +26,7 @@
val STRING = Value("string")
val ALT_STRING = Value("back-quoted string")
val VERBATIM = Value("verbatim text")
- val CARTOUCHE = Value("cartouche")
+ val CARTOUCHE = Value("text cartouche")
val SPACE = Value("white space")
val COMMENT = Value("comment text")
val ERROR = Value("bad input")
@@ -102,16 +102,16 @@
def token(lexicon: Scan.Lexicon, is_command: String => Boolean): Parser[Token] =
delimited_token | other_token(lexicon, is_command)
- def token_context(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Context)
- : Parser[(Token, Scan.Context)] =
+ def token_line(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Line_Context)
+ : Parser[(Token, Scan.Line_Context)] =
{
val string =
- quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
+ quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
val alt_string =
- quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
- val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
- val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
- val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
+ quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
+ val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
+ val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
+ val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
val other = other_token(lexicon, is_command) ^^ { case x => (x, Scan.Finished) }
string | (alt_string | (verb | (cart | (cmt | other))))
--- a/src/Pure/ML/ml_lex.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala Sun Feb 16 17:50:13 2014 +0100
@@ -51,6 +51,13 @@
val STRING = Value("quoted string")
val SPACE = Value("white space")
val COMMENT = Value("comment text")
+ val ANTIQ = Value("antiquotation")
+ val ANTIQ_START = Value("antiquotation: start")
+ val ANTIQ_STOP = Value("antiquotation: stop")
+ val ANTIQ_OTHER = Value("antiquotation: other")
+ val ANTIQ_STRING = Value("antiquotation: quoted string")
+ val ANTIQ_ALT_STRING = Value("antiquotation: back-quoted string")
+ val ANTIQ_CARTOUCHE = Value("antiquotation: text cartouche")
val ERROR = Value("bad input")
}
@@ -64,9 +71,10 @@
/** parsers **/
- case object ML_String extends Scan.Context
+ case object ML_String extends Scan.Line_Context
+ case class Antiq(ctxt: Scan.Line_Context) extends Scan.Line_Context
- private object Parsers extends Scan.Parsers
+ private object Parsers extends Scan.Parsers with Antiquote.Parsers
{
/* string material */
@@ -107,9 +115,9 @@
private val ml_string: Parser[Token] =
"\"" ~ ml_string_body ~ "\"" ^^ { case x ~ y ~ z => Token(Kind.STRING, x + y + z) }
- private def ml_string_context(ctxt: Scan.Context): Parser[(Token, Scan.Context)] =
+ private def ml_string_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
{
- def result(x: String, c: Scan.Context) = (Token(Kind.STRING, x), c)
+ def result(x: String, c: Scan.Line_Context) = (Token(Kind.STRING, x), c)
ctxt match {
case Scan.Finished =>
@@ -130,8 +138,8 @@
private val ml_comment: Parser[Token] =
comment ^^ (x => Token(Kind.COMMENT, x))
- private def ml_comment_context(ctxt: Scan.Context): Parser[(Token, Scan.Context)] =
- comment_context(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) }
+ private def ml_comment_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+ comment_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) }
/* delimited token */
@@ -192,22 +200,52 @@
val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x))
+ val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x))
+
val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x))
- space | (recover_delimited |
- (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))
+ space | (recover_delimited | (ml_antiq |
+ (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))
}
+ /* antiquotations (line-oriented) */
+
+ def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+ ctxt match {
+ case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished)))
+ case _ => failure("")
+ }
+
+ def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+ ctxt match {
+ case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished))
+ case _ => failure("")
+ }
+
+ def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+ context match {
+ case Antiq(ctxt) =>
+ (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context))
+ else failure("")) |
+ quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } |
+ quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } |
+ cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) }
+ case _ => failure("")
+ }
+
+
/* token */
def token: Parser[Token] = delimited_token | other_token
- def token_context(ctxt: Scan.Context): Parser[(Token, Scan.Context)] =
+ def token_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
{
val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished))
- ml_string_context(ctxt) | (ml_comment_context(ctxt) | other)
+ ml_string_line(ctxt) |
+ (ml_comment_line(ctxt) |
+ (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
}
}
@@ -222,13 +260,14 @@
}
}
- def tokenize_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) =
+ def tokenize_line(input: CharSequence, context: Scan.Line_Context)
+ : (List[Token], Scan.Line_Context) =
{
var in: Reader[Char] = new CharSequenceReader(input)
val toks = new mutable.ListBuffer[Token]
var ctxt = context
while (!in.atEnd) {
- Parsers.parse(Parsers.token_context(ctxt), in) match {
+ Parsers.parse(Parsers.token_line(ctxt), in) match {
case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
case Parsers.NoSuccess(_, rest) =>
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
--- a/src/Pure/ML/ml_thms.ML Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML Sun Feb 16 17:50:13 2014 +0100
@@ -35,7 +35,7 @@
(* attribute source *)
val _ = Theory.setup
- (ML_Context.add_antiq (Binding.name "attributes")
+ (ML_Context.add_antiq @{binding attributes}
(Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
let
val ctxt = Context.the_proof context;
@@ -73,10 +73,10 @@
in (Context.Proof ctxt'', decl) end;
val _ = Theory.setup
- (ML_Context.add_antiq (Binding.name "thm")
+ (ML_Context.add_antiq @{binding thm}
(Scan.depend (fn context =>
Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
- ML_Context.add_antiq (Binding.name "thms")
+ ML_Context.add_antiq @{binding thms}
(Scan.depend (fn context =>
Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
@@ -86,17 +86,24 @@
val and_ = Args.$$$ "and";
val by = Args.$$$ "by";
val goal = Scan.unless (by || and_) Args.name_inner_syntax;
+val goals1 = Scan.repeat1 goal;
val _ = Theory.setup
- (ML_Context.add_antiq (Binding.name "lemma")
+ (ML_Context.add_antiq @{binding lemma}
(Scan.depend (fn context =>
- Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
- (by |-- Method.parse -- Scan.option Method.parse) >>
- (fn ((is_open, raw_propss), methods) =>
+ Args.mode "open" -- goals1 -- Scan.repeat (Parse.position and_ -- Parse.!!! goals1) --
+ (Parse.position by -- (Method.parse -- Scan.option Method.parse)) >>
+ (fn (((is_open, raw_props), and_propss), ((_, by_pos), methods)) =>
let
val ctxt = Context.proof_of context;
- val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+ val reports =
+ (by_pos, Markup.keyword1) ::
+ map (fn ((_, and_pos), _) => (and_pos, Markup.keyword2)) and_propss;
+ val _ = Context_Position.reports ctxt reports;
+
+ val propss =
+ burrow (map (rpair []) o Syntax.read_props ctxt) (raw_props :: map #2 and_propss);
val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
fun after_qed res goal_ctxt =
Proof_Context.put_thms false (Auto_Bind.thisN,
--- a/src/Pure/Pure.thy Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/Pure.thy Sun Feb 16 17:50:13 2014 +0100
@@ -101,6 +101,7 @@
"ProofGeneral.inform_file_retracted" :: control
begin
+ML_file "ML/ml_thms.ML"
ML_file "Isar/isar_syn.ML"
ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
--- a/src/Pure/ROOT Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/ROOT Sun Feb 16 17:50:13 2014 +0100
@@ -151,7 +151,6 @@
"ML/ml_statistics_dummy.ML"
"ML/ml_statistics_polyml-5.5.0.ML"
"ML/ml_syntax.ML"
- "ML/ml_thms.ML"
"PIDE/active.ML"
"PIDE/command.ML"
"PIDE/document.ML"
--- a/src/Pure/ROOT.ML Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/ROOT.ML Sun Feb 16 17:50:13 2014 +0100
@@ -260,7 +260,6 @@
use "Isar/spec_rules.ML";
use "Isar/specification.ML";
use "Isar/typedecl.ML";
-use "ML/ml_thms.ML";
(*toplevel transactions*)
use "Isar/proof_node.ML";
--- a/src/Pure/build-jars Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Pure/build-jars Sun Feb 16 17:50:13 2014 +0100
@@ -13,6 +13,7 @@
Concurrent/future.scala
Concurrent/simple_thread.scala
Concurrent/volatile.scala
+ General/antiquote.scala
General/bytes.scala
General/exn.scala
General/file.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Feb 16 17:50:13 2014 +0100
@@ -148,9 +148,15 @@
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
- Swing_Thread.now { Document_Model(buffer) } match {
- case Some(model) if model.is_theory =>
- val snapshot = model.snapshot
+ val opt_snapshot =
+ Swing_Thread.now {
+ Document_Model(buffer) match {
+ case Some(model) if model.is_theory => Some(model.snapshot)
+ case _ => None
+ }
+ }
+ opt_snapshot match {
+ case Some(snapshot) =>
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
Isabelle_Sidekick.swing_markup_tree(
@@ -172,7 +178,7 @@
})
}
true
- case _ => false
+ case None => false
}
}
}
--- a/src/Tools/jEdit/src/rendering.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sun Feb 16 17:50:13 2014 +0100
@@ -129,6 +129,13 @@
ML_Lex.Kind.STRING -> LITERAL1,
ML_Lex.Kind.SPACE -> NULL,
ML_Lex.Kind.COMMENT -> COMMENT1,
+ ML_Lex.Kind.ANTIQ -> NULL,
+ ML_Lex.Kind.ANTIQ_START -> LITERAL4,
+ ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
+ ML_Lex.Kind.ANTIQ_OTHER -> NULL,
+ ML_Lex.Kind.ANTIQ_STRING -> NULL,
+ ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
+ ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
ML_Lex.Kind.ERROR -> INVALID
).withDefaultValue(NULL)
}
@@ -599,7 +606,7 @@
private val foreground_include =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
+ Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ)
def foreground(range: Text.Range): List[Text.Info[Color]] =
snapshot.select_markup(range, Some(foreground_include), _ =>
@@ -617,6 +624,7 @@
Markup.STRING -> Color.BLACK,
Markup.ALTSTRING -> Color.BLACK,
Markup.VERBATIM -> Color.BLACK,
+ Markup.CARTOUCHE -> Color.BLACK,
Markup.LITERAL -> keyword1_color,
Markup.DELIMITER -> Color.BLACK,
Markup.TFREE -> tfree_color,
--- a/src/Tools/jEdit/src/token_markup.scala Sun Feb 16 13:56:48 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Sun Feb 16 17:50:13 2014 +0100
@@ -177,7 +177,7 @@
private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
- private class Line_Context(val context: Option[Scan.Context])
+ private class Line_Context(val context: Option[Scan.Line_Context])
extends TokenMarker.LineContext(isabelle_rules, null)
{
override def hashCode: Int = context.hashCode
@@ -204,14 +204,14 @@
{
val (styled_tokens, context1) =
if (mode == "isabelle-ml") {
- val (tokens, ctxt1) = ML_Lex.tokenize_context(line, line_ctxt.get)
+ val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
(styled_tokens, new Line_Context(Some(ctxt1)))
}
else {
Isabelle.mode_syntax(mode) match {
case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
- val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+ val (tokens, ctxt1) = syntax.scan_line(line, line_ctxt.get)
val styled_tokens =
tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
(styled_tokens, new Line_Context(Some(ctxt1)))