--- a/src/Doc/antiquote_setup.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Wed Dec 03 22:44:24 2014 +0100
@@ -62,7 +62,8 @@
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
| ml_functor _ = raise Fail "Bad ML functor specification";
-val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);
+val is_name =
+ ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
fun ml_name txt =
(case filter is_name (ML_Lex.tokenize txt) of
@@ -203,7 +204,7 @@
Keyword.is_command keywords name andalso
let
val markup =
- Outer_Syntax.scan keywords Position.none name
+ Token.explode keywords Position.none name
|> maps (Outer_Syntax.command_reports thy)
|> map (snd o fst);
val _ = Context_Position.reports ctxt (map (pair pos) markup);
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 03 22:44:24 2014 +0100
@@ -534,8 +534,8 @@
let
fun do_method named_thms ctxt =
let
- val ref_of_str =
- suffix ";" #> Outer_Syntax.scan (Thy_Header.get_keywords' ctxt) Position.none
+ val ref_of_str = (* FIXME proper wrapper for parser combinators *)
+ suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none
#> Parse.xthm #> fst
val thms = named_thms |> maps snd
val facts = named_thms |> map (ref_of_str o fst o fst)
@@ -561,7 +561,7 @@
let
val (type_encs, lam_trans) =
!meth
- |> Outer_Syntax.scan (Thy_Header.get_keywords' ctxt) Position.start
+ |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Dec 03 22:44:24 2014 +0100
@@ -221,7 +221,8 @@
val thy = Proof_Context.theory_of lthy
val dummy_thm = Thm.transfer thy Drule.dummy_thm
- val pointer = Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none bundle_name
+ val pointer =
+ Token.explode (Thy_Header.get_keywords thy) Position.none (cartouche bundle_name)
val restore_lifting_att =
([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
in
@@ -920,7 +921,8 @@
val lifting_restore_internal_attribute_setup =
Attrib.setup @{binding lifting_restore_internal}
- (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
+ (Scan.lift Parse.cartouche >>
+ (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
"restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
val _ = Theory.setup lifting_restore_internal_attribute_setup
@@ -969,7 +971,7 @@
case bundle of
[(_, [arg_src])] =>
let
- val (name, _) = Token.syntax (Scan.lift Args.name) arg_src ctxt
+ val (name, _) = Token.syntax (Scan.lift Parse.cartouche) arg_src ctxt
handle ERROR _ => error "The provided bundle is not a lifting bundle."
in name end
| _ => error "The provided bundle is not a lifting bundle."
--- a/src/HOL/Tools/try0.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/HOL/Tools/try0.ML Wed Dec 03 22:44:24 2014 +0100
@@ -43,7 +43,7 @@
fun parse_method keywords s =
enclose "(" ")" s
- |> Outer_Syntax.scan keywords Position.start
+ |> Token.explode keywords Position.start
|> filter Token.is_proper
|> Scan.read Token.stopper Method.parse
|> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
--- a/src/Pure/GUI/gui.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/GUI/gui.scala Wed Dec 03 22:44:24 2014 +0100
@@ -60,13 +60,11 @@
if (Platform.is_windows || Platform.is_macos) None
else
try {
- val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
- val getWM = XWM.getDeclaredMethod("getWM")
- getWM.setAccessible(true)
- getWM.invoke(null) match {
- case null => None
- case wm => Some(wm.toString)
- }
+ val wm =
+ Untyped.method(Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader),
+ "getWM").invoke(null)
+ if (wm == null) None
+ else Some(wm.toString)
}
catch {
case _: ClassNotFoundException => None
--- a/src/Pure/General/completion.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/General/completion.scala Wed Dec 03 22:44:24 2014 +0100
@@ -276,12 +276,35 @@
}
final class Completion private(
- keywords: Map[String, Boolean] = Map.empty,
- words_lex: Scan.Lexicon = Scan.Lexicon.empty,
- words_map: Multi_Map[String, String] = Multi_Map.empty,
- abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
- abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
+ protected val keywords: Map[String, Boolean] = Map.empty,
+ protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
+ protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
+ protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
+ protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
{
+ /* merge */
+
+ def is_empty: Boolean =
+ keywords.isEmpty &&
+ words_lex.is_empty &&
+ words_map.isEmpty &&
+ abbrevs_lex.is_empty &&
+ abbrevs_map.isEmpty
+
+ def ++ (other: Completion): Completion =
+ if (this eq other) this
+ else if (is_empty) other
+ else {
+ val keywords1 =
+ (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ val words_lex1 = words_lex ++ other.words_lex
+ val words_map1 = words_map ++ other.words_map
+ val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
+ val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
+ new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+ }
+
+
/* keywords */
private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
--- a/src/Pure/General/multi_map.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/General/multi_map.scala Wed Dec 03 22:44:24 2014 +0100
@@ -21,7 +21,7 @@
}
-final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
+final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]])
extends scala.collection.immutable.Map[A, B]
with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
{
@@ -50,6 +50,14 @@
else this
}
+ def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] =
+ if (this eq other) this
+ else if (isEmpty) other
+ else
+ (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
+ case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
+ }
+
/* Map operations */
--- a/src/Pure/General/position.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/General/position.ML Wed Dec 03 22:44:24 2014 +0100
@@ -14,6 +14,7 @@
val end_offset_of: T -> int option
val file_of: T -> string option
val advance: Symbol.symbol -> T -> T
+ val advance_offset: int -> T -> T
val distance_of: T -> T -> int
val none: T
val start: T
@@ -101,6 +102,11 @@
fun advance sym (pos as (Pos (count, props))) =
if invalid_count count then pos else Pos (advance_count sym count, props);
+fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
+ if invalid_count count then pos
+ else if valid i then raise Fail "Illegal line position"
+ else Pos ((i, if_valid j (j + offset), k), props);
+
(* distance of adjacent positions *)
--- a/src/Pure/General/scan.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/General/scan.ML Wed Dec 03 22:44:24 2014 +0100
@@ -280,6 +280,7 @@
datatype lexicon = Lexicon of (bool * lexicon) Symtab.table;
val empty_lexicon = Lexicon Symtab.empty;
+fun is_empty_lexicon (Lexicon tab) = Symtab.is_empty tab;
fun is_literal _ [] = false
| is_literal (Lexicon tab) (c :: cs) =
@@ -328,7 +329,11 @@
in append (if tip then rev path' :: content else content) end) tab [];
val dest_lexicon = map implode o dest [];
-fun merge_lexicons (lex1, lex2) = fold extend_lexicon (dest [] lex2) lex1;
+
+fun merge_lexicons (lex1, lex2) =
+ if pointer_eq (lex1, lex2) then lex1
+ else if is_empty_lexicon lex1 then lex2
+ else fold extend_lexicon (dest [] lex2) lex1;
end;
--- a/src/Pure/General/scan.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/General/scan.scala Wed Dec 03 22:44:24 2014 +0100
@@ -318,10 +318,10 @@
{
/* auxiliary operations */
- private def content(tree: Lexicon.Tree, result: List[String]): List[String] =
+ private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
(result /: tree.branches.toList) ((res, entry) =>
entry match { case (_, (s, tr)) =>
- if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
+ if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
{
@@ -341,20 +341,20 @@
def completions(str: CharSequence): List[String] =
lookup(str) match {
- case Some((true, tree)) => content(tree, List(str.toString))
- case Some((false, tree)) => content(tree, Nil)
+ case Some((true, tree)) => dest(tree, List(str.toString))
+ case Some((false, tree)) => dest(tree, Nil)
case None => Nil
}
/* pseudo Set methods */
- def iterator: Iterator[String] = content(rep, Nil).sorted.iterator
+ def raw_iterator: Iterator[String] = dest(rep, Nil).iterator
+ def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator
override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
- def empty: Lexicon = Lexicon.empty
- def isEmpty: Boolean = rep.branches.isEmpty
+ def is_empty: Boolean = rep.branches.isEmpty
def contains(elem: String): Boolean =
lookup(elem) match {
@@ -363,7 +363,7 @@
}
- /* add elements */
+ /* build lexicon */
def + (elem: String): Lexicon =
if (contains(elem)) this
@@ -388,6 +388,11 @@
def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
+ def ++ (other: Lexicon): Lexicon =
+ if (this eq other) this
+ else if (is_empty) other
+ else this ++ other.raw_iterator
+
/* scan */
--- a/src/Pure/General/untyped.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/General/untyped.scala Wed Dec 03 22:44:24 2014 +0100
@@ -8,8 +8,18 @@
package isabelle
+import java.lang.reflect.Method
+
+
object Untyped
{
+ def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
+ {
+ val m = c.getDeclaredMethod(name, arg_types: _*)
+ m.setAccessible(true)
+ m
+ }
+
def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
private var next_elem: Class[_ <: AnyRef] = obj.getClass
def hasNext(): Boolean = next_elem != null
@@ -20,8 +30,8 @@
}
}
- def get(obj: AnyRef, x: String): AnyRef =
- if (obj == null) null
+ def get[A](obj: AnyRef, x: String): A =
+ if (obj == null) null.asInstanceOf[A]
else {
val iterator =
for {
@@ -32,7 +42,7 @@
field.setAccessible(true)
field.get(obj)
}
- if (iterator.hasNext) iterator.next
+ if (iterator.hasNext) iterator.next.asInstanceOf[A]
else error("No field " + quote(x) + " for " + obj)
}
}
--- a/src/Pure/Isar/keyword.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Isar/keyword.scala Wed Dec 03 22:44:24 2014 +0100
@@ -83,12 +83,8 @@
class Keywords private(
val minor: Scan.Lexicon = Scan.Lexicon.empty,
val major: Scan.Lexicon = Scan.Lexicon.empty,
- commands: Map[String, (String, List[String])] = Map.empty)
+ protected val commands: Map[String, (String, List[String])] = Map.empty)
{
- /* content */
-
- def is_empty: Boolean = minor.isEmpty && major.isEmpty
-
override def toString: String =
{
val keywords1 = minor.iterator.map(quote(_)).toList
@@ -101,6 +97,24 @@
}
+ /* merge */
+
+ def is_empty: Boolean = minor.is_empty && major.is_empty
+
+ def ++ (other: Keywords): Keywords =
+ if (this eq other) this
+ else if (is_empty) other
+ else {
+ val minor1 = minor ++ other.minor
+ val major1 = major ++ other.major
+ val commands1 =
+ if (commands eq other.commands) commands
+ else if (commands.isEmpty) other.commands
+ else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ new Keywords(minor1, major1, commands1)
+ }
+
+
/* add keywords */
def + (name: String): Keywords = new Keywords(minor + name, major, commands)
--- a/src/Pure/Isar/outer_syntax.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Wed Dec 03 22:44:24 2014 +0100
@@ -19,7 +19,6 @@
(bool -> local_theory -> Proof.state) parser -> unit
val local_theory_to_proof: command_spec -> string ->
(local_theory -> Proof.state) parser -> unit
- val scan: Keyword.keywords -> Position.T -> string -> Token.T list
val parse: theory -> Position.T -> string -> Toplevel.transition list
val parse_tokens: theory -> Token.T list -> Toplevel.transition list
val parse_spans: Token.T list -> Command_Span.span list
@@ -148,15 +147,6 @@
(** toplevel parsing **)
-(* scan tokens *)
-
-fun scan keywords pos =
- Source.of_string #>
- Symbol.source #>
- Token.source keywords pos #>
- Source.exhaust;
-
-
(* parse commands *)
local
--- a/src/Pure/Isar/outer_syntax.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Wed Dec 03 22:44:24 2014 +0100
@@ -7,7 +7,6 @@
package isabelle
-import scala.util.parsing.input.{Reader, CharSequenceReader}
import scala.collection.mutable
import scala.annotation.tailrec
@@ -112,6 +111,18 @@
}
+ /* merge */
+
+ def ++ (other: Prover.Syntax): Prover.Syntax =
+ if (this eq other) this
+ else {
+ val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
+ val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
+ if ((keywords eq keywords1) && (completion eq completion1)) this
+ else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
+ }
+
+
/* load commands */
def load_command(name: String): Option[List[String]] = keywords.load_command(name)
@@ -172,33 +183,6 @@
}
- /* token language */
-
- def scan(input: CharSequence): List[Token] =
- {
- val in: Reader[Char] = new CharSequenceReader(input)
- Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match {
- case Token.Parsers.Success(tokens, _) => tokens
- case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
- }
- }
-
- 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_line(keywords, 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)
- }
- }
- (toks.toList, ctxt)
- }
-
-
/* command spans */
def parse_spans(toks: List[Token]): List[Command_Span.Span] =
@@ -237,7 +221,7 @@
}
def parse_spans(input: CharSequence): List[Command_Span.Span] =
- parse_spans(scan(input))
+ parse_spans(Token.explode(keywords, input))
/* overall document structure */
--- a/src/Pure/Isar/parse.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Isar/parse.ML Wed Dec 03 22:44:24 2014 +0100
@@ -185,15 +185,15 @@
val command_ = kind Token.Command;
val keyword = kind Token.Keyword;
val short_ident = kind Token.Ident;
-val long_ident = kind Token.LongIdent;
-val sym_ident = kind Token.SymIdent;
+val long_ident = kind Token.Long_Ident;
+val sym_ident = kind Token.Sym_Ident;
val term_var = kind Token.Var;
-val type_ident = kind Token.TypeIdent;
-val type_var = kind Token.TypeVar;
+val type_ident = kind Token.Type_Ident;
+val type_var = kind Token.Type_Var;
val number = kind Token.Nat;
val float_number = kind Token.Float;
val string = kind Token.String;
-val alt_string = kind Token.AltString;
+val alt_string = kind Token.Alt_String;
val verbatim = kind Token.Verbatim;
val cartouche = kind Token.Cartouche;
val eof = kind Token.EOF;
@@ -405,8 +405,8 @@
local
val argument_kinds =
- [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
- Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
+ [Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var,
+ Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim];
fun arguments is_symid =
let
--- a/src/Pure/Isar/token.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Isar/token.ML Wed Dec 03 22:44:24 2014 +0100
@@ -7,9 +7,13 @@
signature TOKEN =
sig
datatype kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
- Error of string | EOF
+ (*immediate source*)
+ Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
+ Float | Space |
+ (*delimited content*)
+ String | Alt_String | Verbatim | Cartouche | Comment |
+ (*special content*)
+ Error of string | Internal_Value | EOF
val str_of_kind: kind -> string
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
type T
@@ -85,6 +89,8 @@
val source_strict: Keyword.keywords ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+ val explode: Keyword.keywords -> Position.T -> string -> T list
+ val make: (int * int) * string -> Position.T -> T * Position.T
type 'a parser = T list -> 'a * T list
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
@@ -101,32 +107,40 @@
(* token kind *)
datatype kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
- Error of string | EOF;
+ (*immediate source*)
+ Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
+ Float | Space |
+ (*delimited content*)
+ String | Alt_String | Verbatim | Cartouche | Comment |
+ (*special content*)
+ Error of string | Internal_Value | EOF;
val str_of_kind =
fn Command => "command"
| Keyword => "keyword"
| Ident => "identifier"
- | LongIdent => "long identifier"
- | SymIdent => "symbolic identifier"
+ | Long_Ident => "long identifier"
+ | Sym_Ident => "symbolic identifier"
| Var => "schematic variable"
- | TypeIdent => "type variable"
- | TypeVar => "schematic type variable"
+ | Type_Ident => "type variable"
+ | Type_Var => "schematic type variable"
| Nat => "natural number"
| Float => "floating-point number"
+ | Space => "white space"
| String => "quoted string"
- | AltString => "back-quoted string"
+ | Alt_String => "back-quoted string"
| Verbatim => "verbatim text"
| Cartouche => "text cartouche"
- | Space => "white space"
| Comment => "comment text"
- | InternalValue => "internal value"
+ | Internal_Value => "internal value"
| Error _ => "bad input"
| EOF => "end-of-input";
-val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
+val immediate_kinds =
+ Vector.fromList
+ [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
+
+val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
(* datatype token *)
@@ -219,7 +233,7 @@
fun is_kind k (Token (_, (k', _), _)) = k = k';
val is_command = is_kind Command;
-val is_name = is_kind Ident orf is_kind SymIdent orf is_kind String orf is_kind Nat;
+val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
| keyword_with _ _ = false;
@@ -279,25 +293,25 @@
local
val token_kind_markup =
- fn Command => (Markup.command, "")
- | Keyword => (Markup.keyword2, "")
- | Ident => (Markup.empty, "")
- | LongIdent => (Markup.empty, "")
- | SymIdent => (Markup.empty, "")
- | Var => (Markup.var, "")
- | TypeIdent => (Markup.tfree, "")
- | TypeVar => (Markup.tvar, "")
- | Nat => (Markup.empty, "")
- | Float => (Markup.empty, "")
- | String => (Markup.string, "")
- | AltString => (Markup.altstring, "")
- | Verbatim => (Markup.verbatim, "")
- | Cartouche => (Markup.cartouche, "")
- | Space => (Markup.empty, "")
- | Comment => (Markup.comment, "")
- | InternalValue => (Markup.empty, "")
- | Error msg => (Markup.bad, msg)
- | EOF => (Markup.empty, "");
+ fn Command => (Markup.command, "")
+ | Keyword => (Markup.keyword2, "")
+ | Ident => (Markup.empty, "")
+ | Long_Ident => (Markup.empty, "")
+ | Sym_Ident => (Markup.empty, "")
+ | Var => (Markup.var, "")
+ | Type_Ident => (Markup.tfree, "")
+ | Type_Var => (Markup.tvar, "")
+ | Nat => (Markup.empty, "")
+ | Float => (Markup.empty, "")
+ | Space => (Markup.empty, "")
+ | String => (Markup.string, "")
+ | Alt_String => (Markup.alt_string, "")
+ | Verbatim => (Markup.verbatim, "")
+ | Cartouche => (Markup.cartouche, "")
+ | Comment => (Markup.comment, "")
+ | Error msg => (Markup.bad, msg)
+ | Internal_Value => (Markup.empty, "")
+ | EOF => (Markup.empty, "");
in
@@ -326,7 +340,7 @@
fun unparse (Token (_, (kind, x), _)) =
(case kind of
String => Symbol_Pos.quote_string_qq x
- | AltString => Symbol_Pos.quote_string_bq x
+ | Alt_String => Symbol_Pos.quote_string_bq x
| Verbatim => enclose "{*" "*}" x
| Cartouche => cartouche x
| Comment => enclose "(*" "*)" x
@@ -366,7 +380,7 @@
(* access values *)
fun make_value name v =
- Token ((name, Position.no_range), (InternalValue, name), Value (SOME v));
+ Token ((name, Position.no_range), (Internal_Value, name), Value (SOME v));
fun get_value (Token (_, _, Value v)) = v
| get_value _ = NONE;
@@ -530,9 +544,9 @@
fun token_range k (pos1, (ss, pos2)) =
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
-fun scan keywords = !!! "bad input"
+fun scan_token keywords = !!! "bad input"
(Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
- Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
+ Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
scan_verbatim >> token_range Verbatim ||
scan_cartouche >> token_range Cartouche ||
scan_comment >> token_range Comment ||
@@ -541,14 +555,14 @@
(Scan.max token_leq
(Scan.literal (Keyword.major_keywords keywords) >> pair Command)
(Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
- (Lexicon.scan_longid >> pair LongIdent ||
+ (Lexicon.scan_longid >> pair Long_Ident ||
Lexicon.scan_id >> pair Ident ||
Lexicon.scan_var >> pair Var ||
- Lexicon.scan_tid >> pair TypeIdent ||
- Lexicon.scan_tvar >> pair TypeVar ||
+ Lexicon.scan_tid >> pair Type_Ident ||
+ Lexicon.scan_tvar >> pair Type_Var ||
Lexicon.scan_float >> pair Float ||
Lexicon.scan_nat >> pair Nat ||
- scan_symid >> pair SymIdent) >> uncurry token));
+ scan_symid >> pair Sym_Ident) >> uncurry token));
fun recover msg =
(Symbol_Pos.recover_string_qq ||
@@ -563,7 +577,7 @@
fun source' strict keywords =
let
- val scan_strict = Scan.bulk (scan keywords);
+ val scan_strict = Scan.bulk (scan_token keywords);
val scan = if strict then scan_strict else Scan.recover scan_strict recover;
in Source.source Symbol_Pos.stopper scan end;
@@ -573,6 +587,31 @@
end;
+(* explode *)
+
+fun explode keywords pos =
+ Source.of_string #>
+ Symbol.source #>
+ source keywords pos #>
+ Source.exhaust;
+
+
+(* make *)
+
+fun make ((k, n), s) pos =
+ let
+ val pos' = Position.advance_offset n pos;
+ val range = Position.range pos pos';
+ val tok =
+ if k < Vector.length immediate_kinds then
+ Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
+ else
+ (case explode Keyword.empty_keywords pos s of
+ [tok] => tok
+ | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot))
+ in (tok, pos') end;
+
+
(** parsers **)
--- a/src/Pure/Isar/token.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Isar/token.scala Wed Dec 03 22:44:24 2014 +0100
@@ -7,12 +7,17 @@
package isabelle
+import scala.collection.mutable
+import scala.util.parsing.input
+
+
object Token
{
/* tokens */
object Kind extends Enumeration
{
+ /*immediate source*/
val COMMAND = Value("command")
val KEYWORD = Value("keyword")
val IDENT = Value("identifier")
@@ -23,12 +28,14 @@
val TYPE_VAR = Value("schematic type variable")
val NAT = Value("natural number")
val FLOAT = Value("floating-point number")
+ val SPACE = Value("white space")
+ /*delimited content*/
val STRING = Value("string")
val ALT_STRING = Value("back-quoted string")
val VERBATIM = Value("verbatim text")
val CARTOUCHE = Value("text cartouche")
- val SPACE = Value("white space")
val COMMENT = Value("comment text")
+ /*special content*/
val ERROR = Value("bad input")
val UNPARSED = Value("unparsed input")
}
@@ -118,6 +125,34 @@
}
+ /* explode */
+
+ def explode(keywords: Keyword.Keywords, inp: CharSequence): List[Token] =
+ {
+ val in: input.Reader[Char] = new input.CharSequenceReader(inp)
+ Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), in) match {
+ case Parsers.Success(tokens, _) => tokens
+ case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString)
+ }
+ }
+
+ def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context)
+ : (List[Token], Scan.Line_Context) =
+ {
+ var in: input.Reader[Char] = new input.CharSequenceReader(inp)
+ val toks = new mutable.ListBuffer[Token]
+ var ctxt = context
+ while (!in.atEnd) {
+ Parsers.parse(Parsers.token_line(keywords, 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)
+ }
+ }
+ (toks.toList, ctxt)
+ }
+
+
/* token reader */
object Pos
--- a/src/Pure/ML/ml_lex.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Wed Dec 03 22:44:24 2014 +0100
@@ -8,7 +8,7 @@
sig
val keywords: string list
datatype token_kind =
- Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
+ Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
Space | Comment | Error of string | EOF
eqtype token
val stopper: token Scan.stopper
@@ -61,7 +61,7 @@
(* datatype token *)
datatype token_kind =
- Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
+ Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
Space | Comment | Error of string | EOF;
datatype token = Token of Position.range * (token_kind * string);
@@ -135,19 +135,19 @@
local
fun token_kind_markup SML =
- fn Keyword => (Markup.empty, "")
- | Ident => (Markup.empty, "")
- | LongIdent => (Markup.empty, "")
- | TypeVar => (Markup.ML_tvar, "")
- | Word => (Markup.ML_numeral, "")
- | Int => (Markup.ML_numeral, "")
- | Real => (Markup.ML_numeral, "")
- | Char => (Markup.ML_char, "")
- | String => (if SML then Markup.SML_string else Markup.ML_string, "")
- | Space => (Markup.empty, "")
- | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
+ fn Keyword => (Markup.empty, "")
+ | Ident => (Markup.empty, "")
+ | Long_Ident => (Markup.empty, "")
+ | Type_Var => (Markup.ML_tvar, "")
+ | Word => (Markup.ML_numeral, "")
+ | Int => (Markup.ML_numeral, "")
+ | Real => (Markup.ML_numeral, "")
+ | Char => (Markup.ML_char, "")
+ | String => (if SML then Markup.SML_string else Markup.ML_string, "")
+ | Space => (Markup.empty, "")
+ | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
| Error msg => (Markup.bad, msg)
- | EOF => (Markup.empty, "");
+ | EOF => (Markup.empty, "");
in
@@ -280,9 +280,9 @@
(scan_word >> token Word ||
scan_real >> token Real ||
scan_int >> token Int ||
- scan_long_ident >> token LongIdent ||
+ scan_long_ident >> token Long_Ident ||
scan_ident >> token Ident ||
- scan_type_var >> token TypeVar));
+ scan_type_var >> token Type_Var));
val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;
--- a/src/Pure/PIDE/command.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/command.scala Wed Dec 03 22:44:24 2014 +0100
@@ -27,8 +27,8 @@
{
type Entry = (Long, XML.Tree)
val empty = new Results(SortedMap.empty)
- def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
- def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
+ def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
+ def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
}
final class Results private(private val rep: SortedMap[Long, XML.Tree])
--- a/src/Pure/PIDE/document.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/document.ML Wed Dec 03 22:44:24 2014 +0100
@@ -8,7 +8,6 @@
signature DOCUMENT =
sig
val timing: bool Unsynchronized.ref
- val init_keywords: unit -> unit
type node_header = string * Thy_Header.header * string list
type overlay = Document_ID.command * (string * string list)
datatype node_edit =
@@ -20,8 +19,8 @@
val init_state: state
val define_blob: string -> string -> state -> state
type blob_digest = (string * string option) Exn.result
- val define_command: Document_ID.command -> string -> blob_digest list -> string ->
- state -> state
+ val define_command: Document_ID.command -> string -> blob_digest list ->
+ ((int * int) * string) list -> state -> state
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -38,17 +37,6 @@
-(** global keywords **)
-
-val global_keywords = Synchronized.var "global_keywords" Keyword.empty_keywords;
-
-fun init_keywords () =
- Synchronized.change global_keywords
- (fn _ =>
- fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
- (Thy_Info.get_names ()) Keyword.empty_keywords);
-
-fun get_keywords () = Synchronized.value global_keywords;
@@ -69,17 +57,19 @@
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
+ keywords: Keyword.keywords option, (*outer syntax keywords*)
perspective: perspective, (*command perspective*)
entries: Command.exec option Entries.T, (*command entries with excecutions*)
result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
-fun make_node (header, perspective, entries, result) =
- Node {header = header, perspective = perspective, entries = entries, result = result};
+fun make_node (header, keywords, perspective, entries, result) =
+ Node {header = header, keywords = keywords, perspective = perspective,
+ entries = entries, result = result};
-fun map_node f (Node {header, perspective, entries, result}) =
- make_node (f (header, perspective, entries, result));
+fun map_node f (Node {header, keywords, perspective, entries, result}) =
+ make_node (f (header, keywords, perspective, entries, result));
fun make_perspective (required, command_ids, overlays) : perspective =
{required = required,
@@ -90,7 +80,7 @@
val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
val no_perspective = make_perspective (false, [], []);
-val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
+val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
not required andalso
@@ -98,8 +88,9 @@
is_none visible_last andalso
Inttab.is_empty overlays;
-fun is_empty_node (Node {header, perspective, entries, result}) =
+fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
header = no_header andalso
+ is_none keywords andalso
is_no_perspective perspective andalso
Entries.is_empty entries andalso
is_none result;
@@ -113,12 +104,21 @@
| _ => Path.current);
fun set_header header =
- map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+ map_node (fn (_, keywords, perspective, entries, result) =>
+ (header, keywords, perspective, entries, result));
+
+fun get_header_raw (Node {header, ...}) = header;
fun get_header (Node {header = (master, header, errors), ...}) =
if null errors then (master, header)
else error (cat_lines errors);
+fun set_keywords keywords =
+ map_node (fn (header, _, perspective, entries, result) =>
+ (header, keywords, perspective, entries, result));
+
+fun get_keywords (Node {keywords, ...}) = keywords;
+
fun read_header node span =
let
val {name = (name, _), imports, keywords} = #2 (get_header node);
@@ -126,8 +126,10 @@
in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
fun get_perspective (Node {perspective, ...}) = perspective;
+
fun set_perspective args =
- map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
+ map_node (fn (header, keywords, _, entries, result) =>
+ (header, keywords, make_perspective args, entries, result));
val required_node = #required o get_perspective;
val visible_command = Inttab.defined o #visible o get_perspective;
@@ -136,7 +138,9 @@
val overlays = Inttab.lookup_list o #overlays o get_perspective;
fun map_entries f =
- map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
+ map_node (fn (header, keywords, perspective, entries, result) =>
+ (header, keywords, perspective, f entries, result));
+
fun get_entries (Node {entries, ...}) = entries;
fun iterate_entries f = Entries.iterate NONE f o get_entries;
@@ -146,8 +150,10 @@
| SOME id => Entries.iterate (SOME id) f entries);
fun get_result (Node {result, ...}) = result;
+
fun set_result result =
- map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+ map_node (fn (header, keywords, perspective, entries, _) =>
+ (header, keywords, perspective, entries, result));
fun changed_result node node' =
(case (get_result node, get_result node') of
@@ -222,21 +228,43 @@
| Deps (master, header, errors) =>
let
val imports = map fst (#imports header);
- val errors1 =
- (Synchronized.change global_keywords (Keyword.add_keywords (#keywords header)); errors)
- handle ERROR msg => errors @ [msg];
val nodes1 = nodes
|> default_node name
|> fold default_node imports;
val nodes2 = nodes1
|> String_Graph.Keys.fold
(fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
- val (nodes3, errors2) =
- (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1)
- handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
- in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end
+ val (nodes3, errors1) =
+ (String_Graph.add_deps_acyclic (name, imports) nodes2, errors)
+ handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs);
+ in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end
| Perspective perspective => update_node name (set_perspective perspective) nodes);
+fun update_keywords name nodes =
+ nodes |> String_Graph.map_node name (fn node =>
+ if is_empty_node node then node
+ else
+ let
+ val (master, header, errors) = get_header_raw node;
+ val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header);
+ val keywords =
+ Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords);
+ val (keywords', errors') =
+ (Keyword.add_keywords (#keywords header) keywords, errors)
+ handle ERROR msg =>
+ (keywords, if member (op =) errors msg then errors else errors @ [msg]);
+ in
+ node
+ |> set_header (master, header, errors')
+ |> set_keywords (SOME keywords')
+ end);
+
+fun edit_keywords edits (Version nodes) =
+ Version
+ (fold update_keywords
+ (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
+ nodes);
+
fun put_node (name, node) (Version nodes) =
let
val nodes1 = update_node name (K node) nodes;
@@ -326,14 +354,14 @@
(* commands *)
-fun define_command command_id name command_blobs text =
+fun define_command command_id name command_blobs toks =
map_state (fn (versions, blobs, commands, execution) =>
let
val id = Document_ID.print command_id;
val span =
Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id)
- (fn () => Outer_Syntax.scan (get_keywords ()) (Position.id id) text) ());
+ (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
val _ =
Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
@@ -562,7 +590,9 @@
fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () =>
let
val old_version = the_version state old_version_id;
- val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
+ val new_version =
+ timeit "Document.edit_nodes"
+ (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
val nodes = nodes_of new_version;
val required = make_required nodes;
@@ -579,7 +609,7 @@
timeit ("Document.update " ^ name) (fn () =>
Runtime.exn_trace_system (fn () =>
let
- val keywords = get_keywords ();
+ val keywords = the_default (Session.get_keywords ()) (get_keywords node);
val imports = map (apsnd Future.join) deps;
val imports_result_changed = exists (#4 o #1 o #2) imports;
val node_required = Symtab.defined required name;
--- a/src/Pure/PIDE/document.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/document.scala Wed Dec 03 22:44:24 2014 +0100
@@ -244,6 +244,7 @@
final class Node private(
val get_blob: Option[Document.Blob] = None,
val header: Node.Header = Node.no_header,
+ val syntax: Option[Prover.Syntax] = None,
val perspective: Node.Perspective_Command = Node.no_perspective_command,
_commands: Node.Commands = Node.Commands.empty)
{
@@ -256,15 +257,18 @@
def commands: Linear_Set[Command] = _commands.commands
def load_commands: List[Command] = _commands.load_commands
- def clear: Node = new Node(header = header)
+ def clear: Node = new Node(header = header, syntax = syntax)
- def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
+ def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
def update_header(new_header: Node.Header): Node =
- new Node(get_blob, new_header, perspective, _commands)
+ new Node(get_blob, new_header, syntax, perspective, _commands)
+
+ def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
+ new Node(get_blob, header, new_syntax, perspective, _commands)
def update_perspective(new_perspective: Node.Perspective_Command): Node =
- new Node(get_blob, header, new_perspective, _commands)
+ new Node(get_blob, header, syntax, new_perspective, _commands)
def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
perspective.required == other_perspective.required &&
@@ -273,7 +277,7 @@
def update_commands(new_commands: Linear_Set[Command]): Node =
if (new_commands eq _commands.commands) this
- else new Node(get_blob, header, perspective, Node.Commands(new_commands))
+ else new Node(get_blob, header, syntax, perspective, Node.Commands(new_commands))
def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
_commands.iterator(i)
@@ -344,14 +348,11 @@
object Version
{
val init: Version = new Version()
-
- def make(syntax: Option[Prover.Syntax], nodes: Nodes): Version =
- new Version(Document_ID.make(), syntax, nodes)
+ def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
}
final class Version private(
val id: Document_ID.Version = Document_ID.none,
- val syntax: Option[Prover.Syntax] = None,
val nodes: Nodes = Nodes.empty)
{
override def toString: String = "Version(" + id + ")"
--- a/src/Pure/PIDE/markup.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Dec 03 22:44:24 2014 +0100
@@ -115,7 +115,7 @@
val text_foldN: string val text_fold: T
val commandN: string val command: T
val stringN: string val string: T
- val altstringN: string val altstring: T
+ val alt_stringN: string val alt_string: T
val verbatimN: string val verbatim: T
val cartoucheN: string val cartouche: T
val commentN: string val comment: T
@@ -463,7 +463,7 @@
val (improperN, improper) = markup_elem "improper";
val (operatorN, operator) = markup_elem "operator";
val (stringN, string) = markup_elem "string";
-val (altstringN, altstring) = markup_elem "altstring";
+val (alt_stringN, alt_string) = markup_elem "alt_string";
val (verbatimN, verbatim) = markup_elem "verbatim";
val (cartoucheN, cartouche) = markup_elem "cartouche";
val (commentN, comment) = markup_elem "comment";
--- a/src/Pure/PIDE/markup.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Dec 03 22:44:24 2014 +0100
@@ -261,7 +261,7 @@
val IMPROPER = "improper"
val OPERATOR = "operator"
val STRING = "string"
- val ALTSTRING = "altstring"
+ val ALT_STRING = "alt_string"
val VERBATIM = "verbatim"
val CARTOUCHE = "cartouche"
val COMMENT = "comment"
--- a/src/Pure/PIDE/protocol.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/protocol.ML Wed Dec 03 22:44:24 2014 +0100
@@ -23,16 +23,12 @@
end);
val _ =
- Isabelle_Process.protocol_command "Document.init_keywords"
- (fn [] => Document.init_keywords ());
-
-val _ =
Isabelle_Process.protocol_command "Document.define_blob"
(fn [digest, content] => Document.change_state (Document.define_blob digest content));
val _ =
Isabelle_Process.protocol_command "Document.define_command"
- (fn [id, name, blobs_yxml, text] =>
+ (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
let
val blobs =
YXML.parse_body blobs_yxml |>
@@ -41,8 +37,10 @@
[fn ([], a) => Exn.Res (pair string (option string) a),
fn ([], a) => Exn.Exn (ERROR (string a))])
end;
+ val toks =
+ (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
in
- Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
+ Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
end);
val _ =
--- a/src/Pure/PIDE/protocol.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Dec 03 22:44:24 2014 +0100
@@ -392,10 +392,21 @@
{ case Exn.Res((a, b)) =>
(Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+
YXML.string_of_body(list(encode_blob)(command.blobs))
}
+
+ val toks = command.span.content
+ val toks_yxml =
+ { import XML.Encode._
+ val encode_tok: T[Token] =
+ (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
+ YXML.string_of_body(list(encode_tok)(toks))
+ }
+
protocol_command("Document.define_command",
- Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
+ (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
+ toks.map(tok => encode(tok.source))): _*)
}
--- a/src/Pure/PIDE/prover.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/prover.scala Wed Dec 03 22:44:24 2014 +0100
@@ -17,6 +17,7 @@
trait Syntax
{
+ def ++ (other: Syntax): Syntax
def add_keywords(keywords: Thy_Header.Keywords): Syntax
def parse_spans(input: CharSequence): List[Command_Span.Span]
def load_command(name: String): Option[List[String]]
--- a/src/Pure/PIDE/resources.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/resources.ML Wed Dec 03 22:44:24 2014 +0100
@@ -151,7 +151,7 @@
fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
(Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
- val toks = Outer_Syntax.scan keywords text_pos text;
+ val toks = Token.explode keywords text_pos text;
val spans = Outer_Syntax.parse_spans toks;
val elements = Thy_Syntax.parse_elements keywords spans;
--- a/src/Pure/PIDE/session.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/session.ML Wed Dec 03 22:44:24 2014 +0100
@@ -8,6 +8,7 @@
sig
val name: unit -> string
val welcome: unit -> string
+ val get_keywords: unit -> Keyword.keywords
val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
(Path.T * Path.T) list -> string -> string * string -> bool -> unit
val finish: unit -> unit
@@ -31,6 +32,12 @@
else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
+(* base syntax *)
+
+val keywords = Unsynchronized.ref Keyword.empty_keywords;
+fun get_keywords () = ! keywords;
+
+
(* init *)
fun init build info info_path doc doc_graph doc_output doc_variants doc_files
@@ -57,6 +64,9 @@
Future.shutdown ();
Event_Timer.shutdown ();
Future.shutdown ();
+ keywords :=
+ fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
+ (Thy_Info.get_names ()) Keyword.empty_keywords;
session_finished := true);
--- a/src/Pure/PIDE/session.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/PIDE/session.scala Wed Dec 03 22:44:24 2014 +0100
@@ -47,7 +47,7 @@
sealed case class Change(
previous: Document.Version,
- syntax_changed: Boolean,
+ syntax_changed: List[Document.Node.Name],
deps_changed: Boolean,
doc_edits: List[Document.Edit_Command],
version: Document.Version)
@@ -231,11 +231,9 @@
private val global_state = Synchronized(Document.State.init)
def current_state(): Document.State = global_state.value
- def recent_syntax(): Prover.Syntax =
- {
- val version = current_state().recent_finished.version.get_finished
- version.syntax getOrElse resources.base_syntax
- }
+ def recent_syntax(name: Document.Node.Name): Prover.Syntax =
+ current_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
+ resources.base_syntax
/* protocol handlers */
@@ -613,7 +611,6 @@
def init_options(options: Options)
{
update_options(options)
- protocol_command("Document.init_keywords")
}
def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
--- a/src/Pure/ROOT.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/ROOT.ML Wed Dec 03 22:44:24 2014 +0100
@@ -315,6 +315,7 @@
use "PIDE/query_operation.ML";
use "PIDE/resources.ML";
use "Thy/thy_info.ML";
+use "PIDE/session.ML";
use "PIDE/document.ML";
(*theory and proof operations*)
@@ -325,7 +326,6 @@
(* Isabelle/Isar system *)
-use "PIDE/session.ML";
use "System/command_line.ML";
use "System/system_channel.ML";
use "System/message_channel.ML";
--- a/src/Pure/System/options.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/System/options.scala Wed Dec 03 22:44:24 2014 +0100
@@ -108,7 +108,7 @@
def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
options: Options, file: Path): Options =
{
- val toks = syntax.scan(File.read(file))
+ val toks = Token.explode(syntax.keywords, File.read(file))
val ops =
parse_all(rep(parser), Token.reader(toks, file.implode)) match {
case Success(result, _) => result
--- a/src/Pure/Thy/latex.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Thy/latex.ML Wed Dec 03 22:44:24 2014 +0100
@@ -128,7 +128,7 @@
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
- else if Token.is_kind Token.AltString tok then
+ else if Token.is_kind Token.Alt_String tok then
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
--- a/src/Pure/Thy/thy_syntax.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Wed Dec 03 22:44:24 2014 +0100
@@ -69,11 +69,9 @@
resources: Resources,
previous: Document.Version,
edits: List[Document.Edit_Text]):
- (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
- List[Document.Edit_Command]) =
+ (List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
{
- var updated_imports = false
- var updated_keywords = false
+ val syntax_changed0 = new mutable.ListBuffer[Document.Node.Name]
var nodes = previous.nodes
val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
@@ -84,32 +82,29 @@
!node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
if (update_header) {
val node1 = node.update_header(header)
- updated_imports = updated_imports || (node.header.imports != node1.header.imports)
- updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
+ if (node.header.imports != node1.header.imports ||
+ node.header.keywords != node1.header.keywords) syntax_changed0 += name
nodes += (name -> node1)
doc_edits += (name -> Document.Node.Deps(header))
}
case _ =>
}
- val (syntax, syntax_changed) =
- previous.syntax match {
- case Some(syntax) if !updated_keywords =>
- (syntax, false)
- case _ =>
- val syntax =
- (resources.base_syntax /: nodes.iterator) {
- case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
- }
- (syntax, true)
- }
+ val syntax_changed = nodes.descendants(syntax_changed0.toList)
- val reparse =
- if (updated_imports || updated_keywords)
- nodes.descendants(doc_edits.iterator.map(_._1).toList)
- else Nil
+ for (name <- syntax_changed) {
+ val node = nodes(name)
+ val syntax =
+ if (node.is_empty) None
+ else {
+ val header = node.header
+ val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
+ Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
+ }
+ nodes += (name -> node.update_syntax(syntax))
+ }
- (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
+ (syntax_changed, nodes, doc_edits.toList)
}
@@ -311,14 +306,13 @@
def get_blob(name: Document.Node.Name) =
doc_blobs.get(name) orElse previous.nodes(name).get_blob
- val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
- header_edits(resources, previous, edits)
+ val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
val (doc_edits, version) =
- if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
+ if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
else {
val reparse =
- (reparse0 /: nodes0.iterator)({
+ (syntax_changed /: nodes0.iterator)({
case (reparse, (name, node)) =>
if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
name :: reparse
@@ -336,6 +330,7 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
+ val syntax = node.syntax getOrElse resources.base_syntax
val commands = node.commands
val node1 =
@@ -354,9 +349,9 @@
nodes += (name -> node2)
}
- (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
+ (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
}
- Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
+ Session.Change(previous, syntax_changed, !syntax_changed.isEmpty, doc_edits, version)
}
}
--- a/src/Pure/Tools/build.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/build.scala Wed Dec 03 22:44:24 2014 +0100
@@ -259,7 +259,7 @@
def parse_entries(root: Path): List[(String, Session_Entry)] =
{
- val toks = root_syntax.scan(File.read(root))
+ val toks = Token.explode(root_syntax.keywords, File.read(root))
parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
case Success(result, _) =>
--- a/src/Pure/Tools/find_consts.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML Wed Dec 03 22:44:24 2014 +0100
@@ -145,7 +145,7 @@
in
fun read_query pos str =
- Outer_Syntax.scan query_keywords pos str
+ Token.explode query_keywords pos str
|> filter Token.is_proper
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
|> #1;
--- a/src/Pure/Tools/find_theorems.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Dec 03 22:44:24 2014 +0100
@@ -531,7 +531,7 @@
in
fun read_query pos str =
- Outer_Syntax.scan query_keywords pos str
+ Token.explode query_keywords pos str
|> filter Token.is_proper
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
|> #1;
--- a/src/Pure/Tools/main.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/main.scala Wed Dec 03 22:44:24 2014 +0100
@@ -122,7 +122,7 @@
val jedit =
Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
- val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
+ val jedit_main = jedit.getMethod("main", classOf[Array[String]])
() => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
}
--- a/src/Pure/Tools/update_cartouches.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Wed Dec 03 22:44:24 2014 +0100
@@ -20,7 +20,7 @@
{
val text0 = File.read(path)
val text1 =
- (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
+ (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
yield {
if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
else if (tok.kind == Token.Kind.VERBATIM) {
--- a/src/Pure/Tools/update_header.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/update_header.scala Wed Dec 03 22:44:24 2014 +0100
@@ -13,7 +13,7 @@
{
val text0 = File.read(path)
val text1 =
- (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
+ (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
yield { if (tok.source == "header") section else tok.source }).mkString
if (text0 != text1) {
--- a/src/Pure/Tools/update_semicolons.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Pure/Tools/update_semicolons.scala Wed Dec 03 22:44:24 2014 +0100
@@ -13,7 +13,7 @@
{
val text0 = File.read(path)
val text1 =
- (for (tok <- Outer_Syntax.empty.scan(text0).iterator if tok.source != ";")
+ (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator if tok.source != ";")
yield tok.source).mkString
if (text0 != text1) {
--- a/src/Tools/Code/code_target.ML Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/Code/code_target.ML Wed Dec 03 22:44:24 2014 +0100
@@ -696,7 +696,7 @@
val thy = Thy_Info.get_theory thyname;
val ctxt = Proof_Context.init_global thy;
val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
- (filter Token.is_proper o Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none);
+ (filter Token.is_proper o Token.explode (Thy_Header.get_keywords thy) Position.none);
in case parse cmd_expr
of SOME f => (writeln "Now generating code..."; f ctxt)
| NONE => error ("Bad directive " ^ quote cmd_expr)
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Wed Dec 03 22:44:24 2014 +0100
@@ -157,7 +157,7 @@
val buffer = text_area.getBuffer
val decode = Isabelle_Encoding.is_active(buffer)
- Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
+ Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
val context =
(for {
--- a/src/Tools/jEdit/src/document_model.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Wed Dec 03 22:44:24 2014 +0100
@@ -13,8 +13,9 @@
import scala.collection.mutable
+import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer, LineManager}
object Document_Model
@@ -44,15 +45,23 @@
}
}
- def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
+ def init(session: Session, buffer: Buffer, node_name: Document.Node.Name,
+ old_model: Option[Document_Model]): Document_Model =
{
GUI_Thread.require {}
- apply(buffer).map(_.deactivate)
- val model = new Document_Model(session, buffer, node_name)
- buffer.setProperty(key, model)
- model.activate()
- buffer.propertiesChanged
- model
+
+ old_model match {
+ case Some(old)
+ if old.node_name == node_name && Isabelle.buffer_token_marker(buffer).isEmpty => old
+
+ case _ =>
+ apply(buffer).map(_.deactivate)
+ val model = new Document_Model(session, buffer, node_name)
+ buffer.setProperty(key, model)
+ model.activate()
+ buffer.propertiesChanged
+ model
+ }
}
}
@@ -275,18 +284,39 @@
}
+ /* syntax */
+
+ def syntax_changed()
+ {
+ Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0)
+ for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
+ Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
+ invoke(text_area)
+ }
+
+ private def init_token_marker()
+ {
+ Isabelle.buffer_token_marker(buffer) match {
+ case Some(marker) if marker != buffer.getTokenMarker =>
+ buffer.setTokenMarker(marker)
+ syntax_changed()
+ case _ =>
+ }
+ }
+
+
/* activation */
private def activate()
{
pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
buffer.addBufferListener(buffer_listener)
- Token_Markup.refresh_buffer(buffer)
+ init_token_marker()
}
private def deactivate()
{
buffer.removeBufferListener(buffer_listener)
- Token_Markup.refresh_buffer(buffer)
+ init_token_marker()
}
}
--- a/src/Tools/jEdit/src/isabelle.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Dec 03 22:44:24 2014 +0100
@@ -15,6 +15,7 @@
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.{jEdit, View, Buffer}
+import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher}
import org.gjt.sp.jedit.syntax.TokenMarker
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
@@ -29,7 +30,6 @@
List(
"isabelle", // theory source
"isabelle-ml", // ML source
- "isabelle-markup", // SideKick markup tree
"isabelle-news", // NEWS
"isabelle-options", // etc/options
"isabelle-output", // pretty text area output
@@ -47,15 +47,9 @@
private lazy val news_syntax: Outer_Syntax =
Outer_Syntax.init().no_tokens
- def session_syntax(): Option[Outer_Syntax] =
- PIDE.session.recent_syntax match {
- case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
- case _ => None
- }
-
- def mode_syntax(name: String): Option[Outer_Syntax] =
- name match {
- case "isabelle" | "isabelle-markup" => session_syntax()
+ def mode_syntax(mode: String): Option[Outer_Syntax] =
+ mode match {
+ case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Build.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
@@ -65,14 +59,30 @@
case _ => None
}
+ def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
+ (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
+ case ("isabelle", Some(model)) =>
+ Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
+ case (mode, _) => mode_syntax(mode)
+ }
+
/* token markers */
- private val markers: Map[String, TokenMarker] =
- Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) +
+ private val mode_markers: Map[String, TokenMarker] =
+ Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
("bibtex" -> new Bibtex_JEdit.Token_Marker)
- def token_marker(name: String): Option[TokenMarker] = markers.get(name)
+ def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)
+
+ def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
+ {
+ val mode = JEdit_Lib.buffer_mode(buffer)
+ val new_token_marker =
+ if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
+ else mode_token_marker(mode)
+ if (new_token_marker == Some(buffer.getTokenMarker)) None else new_token_marker
+ }
/* structure matchers */
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Dec 03 22:44:24 2014 +0100
@@ -83,7 +83,7 @@
// FIXME lock buffer (!??)
val data = Isabelle_Sidekick.root_data(buffer)
- val syntax = Isabelle.mode_syntax(name)
+ val syntax = Isabelle.buffer_syntax(buffer)
val ok =
if (syntax.isDefined) {
val ok = parser(buffer, syntax.get, data)
@@ -153,7 +153,7 @@
{
val opt_snapshot =
GUI_Thread.now {
- Document_Model(buffer) match {
+ PIDE.document_model(buffer) match {
case Some(model) if model.is_theory => Some(model.snapshot)
case _ => None
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Dec 03 22:44:24 2014 +0100
@@ -128,10 +128,7 @@
{
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
if (navigator != null) {
- try {
- val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
- m.invoke(null, view)
- }
+ try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
catch { case _: NoSuchMethodException => }
}
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Dec 03 22:44:24 2014 +0100
@@ -20,6 +20,7 @@
import org.gjt.sp.jedit.gui.KeyEventWorkaround
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.TokenMarker
object JEdit_Lib
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Dec 03 22:44:24 2014 +0100
@@ -114,7 +114,15 @@
override def commit(change: Session.Change)
{
- if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() }
+ if (!change.syntax_changed.isEmpty)
+ GUI_Thread.later {
+ val changed = change.syntax_changed.toSet
+ for {
+ buffer <- JEdit_Lib.jedit_buffers()
+ model <- PIDE.document_model(buffer)
+ if changed(model.node_name)
+ } model.syntax_changed()
+ }
if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
}
}
--- a/src/Tools/jEdit/src/pide_docking_framework.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/pide_docking_framework.scala Wed Dec 03 22:44:24 2014 +0100
@@ -36,21 +36,18 @@
val detach_operation: Option[() => Unit] =
container match {
case floating: FloatingWindowContainer =>
- val entry = Untyped.get(floating, "entry")
- val win = Untyped.get(entry, "win")
- win match {
+ Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
case dockable: Dockable => dockable.detach_operation
case _ => None
}
case panel: PanelWindowContainer =>
- val entries =
- Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
+ val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
val wins =
(for {
entry <- entries.iterator
- if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
- win = Untyped.get(entry, "win")
+ if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name
+ win = Untyped.get[Any](entry, "win")
if win != null
} yield win).toList
wins match {
--- a/src/Tools/jEdit/src/plugin.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Dec 03 22:44:24 2014 +0100
@@ -17,6 +17,7 @@
import org.jedit.options.CombinedOptions
import org.gjt.sp.jedit.gui.AboutDialog
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.syntax.ModeProvider
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
@@ -64,7 +65,11 @@
/* document model and view */
- def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
+ def document_model(buffer: JEditBuffer): Option[Document_Model] =
+ buffer match {
+ case b: Buffer => Document_Model(b)
+ case _ => None
+ }
def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
@@ -111,11 +116,7 @@
} {
JEdit_Lib.buffer_lock(buffer) {
val node_name = resources.node_name(buffer)
- val model =
- document_model(buffer) match {
- case Some(model) if model.node_name == node_name => model
- case _ => Document_Model.init(session, buffer, node_name)
- }
+ val model = Document_Model.init(session, buffer, node_name, document_model(buffer))
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
if document_view(text_area).map(_.model) != Some(model)
@@ -315,7 +316,6 @@
"It is for testing only, not for production use.")
}
-
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED ||
msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Dec 03 22:44:24 2014 +0100
@@ -43,7 +43,7 @@
val nodes0 = version0.nodes
val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
- val version1 = Document.Version.make(version0.syntax, nodes1)
+ val version1 = Document.Version.make(nodes1)
val state1 =
state0.continue_history(Future.value(version0), edits, Future.value(version1))
.define_version(version1, state0.the_assignment(version0))
@@ -261,7 +261,7 @@
getPainter.setStructureHighlightEnabled(false)
getPainter.setLineHighlightEnabled(false)
- getBuffer.setTokenMarker(Isabelle.token_marker("isabelle-output").get)
+ getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
getBuffer.setReadOnly(true)
getBuffer.setStringProperty("noWordSep", "_'.?")
--- a/src/Tools/jEdit/src/rendering.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Wed Dec 03 22:44:24 2014 +0100
@@ -74,11 +74,11 @@
Token.Kind.TYPE_VAR -> NULL,
Token.Kind.NAT -> NULL,
Token.Kind.FLOAT -> NULL,
+ Token.Kind.SPACE -> NULL,
Token.Kind.STRING -> LITERAL1,
Token.Kind.ALT_STRING -> LITERAL2,
Token.Kind.VERBATIM -> COMMENT3,
Token.Kind.CARTOUCHE -> COMMENT4,
- Token.Kind.SPACE -> NULL,
Token.Kind.COMMENT -> COMMENT1,
Token.Kind.ERROR -> INVALID
).withDefaultValue(NULL)
@@ -132,7 +132,7 @@
Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
private val language_context_elements =
- Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
@@ -194,7 +194,7 @@
active_elements
private val foreground_elements =
- Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.ANTIQUOTED)
private val bullet_elements =
@@ -704,7 +704,7 @@
Markup.IMPROPER -> improper_color,
Markup.OPERATOR -> operator_color,
Markup.STRING -> Color.BLACK,
- Markup.ALTSTRING -> Color.BLACK,
+ Markup.ALT_STRING -> Color.BLACK,
Markup.VERBATIM -> Color.BLACK,
Markup.CARTOUCHE -> Color.BLACK,
Markup.LITERAL -> keyword1_color,
--- a/src/Tools/jEdit/src/spell_checker.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/spell_checker.scala Wed Dec 03 22:44:24 2014 +0100
@@ -255,17 +255,14 @@
factory_cons.setAccessible(true)
val factory = factory_cons.newInstance()
- val add = factory_class.getDeclaredMethod("add", classOf[String])
- add.setAccessible(true)
+ val add = Untyped.method(factory_class, "add", classOf[String])
for {
word <- main_dictionary.iterator ++ included_iterator()
if !excluded(word)
} add.invoke(factory, word)
- val create = factory_class.getDeclaredMethod("create")
- create.setAccessible(true)
- dict = create.invoke(factory)
+ dict = Untyped.method(factory_class, "create").invoke(factory)
}
load()
@@ -299,10 +296,7 @@
if (include) {
if (permanent) save()
-
- val m = dict.getClass.getDeclaredMethod("add", classOf[String])
- m.setAccessible(true)
- m.invoke(dict, word)
+ Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
}
else { save(); load() }
}
@@ -320,11 +314,8 @@
/* check known words */
def contains(word: String): Boolean =
- {
- val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
- m.setAccessible(true)
- m.invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
- }
+ Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
+ invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
def check(word: String): Boolean =
word match {
@@ -342,10 +333,9 @@
private def suggestions(word: String): Option[List[String]] =
{
- val m = dict.getClass.getSuperclass.getDeclaredMethod("searchSuggestions", classOf[String])
- m.setAccessible(true)
val res =
- m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+ Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
+ invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
if (res.isEmpty) None else Some(res)
}
--- a/src/Tools/jEdit/src/structure_matching.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala Wed Dec 03 22:44:24 2014 +0100
@@ -40,7 +40,7 @@
val caret_line = text_area.getCaretLine
val caret = text_area.getCaretPosition
- Isabelle.session_syntax() match {
+ Isabelle.buffer_syntax(text_area.getBuffer) match {
case Some(syntax) =>
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
@@ -143,7 +143,7 @@
{
def get_span(offset: Text.Offset): Option[Text.Range] =
for {
- syntax <- Isabelle.session_syntax()
+ syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
} yield span.range
--- a/src/Tools/jEdit/src/token_markup.scala Wed Dec 03 17:08:24 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Dec 03 22:44:24 2014 +0100
@@ -14,7 +14,7 @@
import java.awt.geom.AffineTransform
import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.{jEdit, Mode}
+import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
import org.gjt.sp.jedit.textarea.{TextArea, Selection}
@@ -193,19 +193,18 @@
}
def buffer_line_context(buffer: JEditBuffer, line: Int): Line_Context =
- Untyped.get(buffer, "lineMgr") match {
- case line_mgr: LineManager =>
- def context =
- line_mgr.getLineContext(line) match {
- case c: Line_Context => Some(c)
- case _ => None
- }
- context getOrElse {
- buffer.markTokens(line, DummyTokenHandler.INSTANCE)
- context getOrElse Line_Context.init
- }
- case _ => Line_Context.init
+ {
+ val line_mgr = Untyped.get[LineManager](buffer, "lineMgr")
+ def context =
+ line_mgr.getLineContext(line) match {
+ case c: Line_Context => Some(c)
+ case _ => None
+ }
+ context getOrElse {
+ buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+ context getOrElse Line_Context.init
}
+ }
/* line tokens */
@@ -219,7 +218,7 @@
for {
ctxt <- line_context.context
text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))
- } yield syntax.scan_line(text, ctxt)._1
+ } yield Token.explode_line(syntax.keywords, text, ctxt)._1
}
def line_token_iterator(
@@ -308,8 +307,23 @@
/* token marker */
- class Marker(mode: String) extends TokenMarker
+ class Marker(
+ protected val mode: String,
+ protected val opt_buffer: Option[Buffer]) extends TokenMarker
{
+ override def hashCode: Int = (mode, opt_buffer).hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer
+ case _ => false
+ }
+
+ override def toString: String =
+ opt_buffer match {
+ case None => "Marker(" + mode + ")"
+ case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
+ }
+
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
{
@@ -319,15 +333,20 @@
val context1 =
{
+ val opt_syntax =
+ opt_buffer match {
+ case Some(buffer) => Isabelle.buffer_syntax(buffer)
+ case None => Isabelle.mode_syntax(mode)
+ }
val (styled_tokens, context1) =
- (line_context.context, Isabelle.mode_syntax(mode)) match {
+ (line_context.context, opt_syntax) match {
case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
(styled_tokens, new Line_Context(Some(ctxt1), structure))
case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
- val (tokens, ctxt1) = syntax.scan_line(line, ctxt)
+ val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
val structure1 = syntax.line_structure(tokens, structure)
val styled_tokens =
tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
@@ -378,17 +397,7 @@
override def loadMode(mode: Mode, xmh: XModeHandler)
{
super.loadMode(mode, xmh)
- Isabelle.token_marker(mode.getName).foreach(mode.setTokenMarker _)
- }
- }
-
- def refresh_buffer(buffer: JEditBuffer)
- {
- Isabelle.token_marker(JEdit_Lib.buffer_mode(buffer)) match {
- case None =>
- case Some(marker) =>
- buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
- buffer.setTokenMarker(marker)
+ Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
}
}
}