--- a/src/Pure/Isar/keyword.ML Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/Isar/keyword.ML Wed Mar 18 13:31:52 2015 +0100
@@ -50,7 +50,6 @@
val is_document_body: keywords -> string -> bool
val is_document_raw: keywords -> string -> bool
val is_document: keywords -> string -> bool
- val is_theory_begin: keywords -> string -> bool
val is_theory_end: keywords -> string -> bool
val is_theory_load: keywords -> string -> bool
val is_theory: keywords -> string -> bool
@@ -219,7 +218,6 @@
val is_document_raw = command_category [document_raw];
val is_document = command_category [document_heading, document_body, document_raw];
-val is_theory_begin = command_category [thy_begin];
val is_theory_end = command_category [thy_end];
val is_theory_load = command_category [thy_load];
--- a/src/Pure/Isar/outer_syntax.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/Isar/outer_syntax.scala Wed Mar 18 13:31:52 2015 +0100
@@ -123,9 +123,7 @@
}
- /* command categories */
-
- def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
+ /* load commands */
def load_command(name: String): Option[List[String]] = keywords.load_command(name)
def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
@@ -230,13 +228,14 @@
def heading_level(command: Command): Option[Int] =
{
- command.name match {
- case "chapter" => Some(0)
- case "section" | "header" => Some(1)
- case "subsection" => Some(2)
- case "subsubsection" => Some(3)
+ val name = command.span.name
+ name match {
+ case Thy_Header.CHAPTER => Some(0)
+ case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
+ case Thy_Header.SUBSECTION => Some(2)
+ case Thy_Header.SUBSUBSECTION => Some(3)
case _ =>
- keywords.command_kind(command.name) match {
+ keywords.command_kind(name) match {
case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
case _ => None
}
@@ -258,7 +257,7 @@
{
stack match {
case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
- body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
+ body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
stack = stack.tail
close(level)
case _ =>
--- a/src/Pure/Isar/token.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/Isar/token.scala Wed Mar 18 13:31:52 2015 +0100
@@ -153,6 +153,15 @@
}
+ /* implode */
+
+ def implode(toks: List[Token]): String =
+ toks match {
+ case List(tok) => tok.source
+ case toks => toks.map(_.source).mkString
+ }
+
+
/* token reader */
object Pos
--- a/src/Pure/PIDE/command.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/PIDE/command.scala Wed Mar 18 13:31:52 2015 +0100
@@ -235,7 +235,7 @@
for {
(chunk_name, chunk) <- command.chunks.iterator
range <- Protocol_Message.positions(
- self_id, command.position, chunk_name, chunk, message)
+ self_id, command.span.position, chunk_name, chunk, message)
} st = st.add_markup(false, chunk_name, Text.Info(range, message2))
}
st
@@ -334,19 +334,15 @@
}
def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
- span.kind match {
- case Command_Span.Command_Span(name, _) =>
- syntax.load_command(name) match {
- case Some(exts) =>
- find_file(clean_tokens(span.content)) match {
- case Some((file, i)) =>
- if (exts.isEmpty) (List(file), i)
- else (exts.map(ext => file + "." + ext), i)
- case None => (Nil, -1)
- }
+ syntax.load_command(span.name) match {
+ case Some(exts) =>
+ find_file(clean_tokens(span.content)) match {
+ case Some((file, i)) =>
+ if (exts.isEmpty) (List(file), i)
+ else (exts.map(ext => file + "." + ext), i)
case None => (Nil, -1)
}
- case _ => (Nil, -1)
+ case None => (Nil, -1)
}
def blobs_info(
@@ -357,12 +353,12 @@
node_name: Document.Node.Name,
span: Command_Span.Span): Blobs_Info =
{
- span.kind match {
+ span.name match {
// inlined errors
- case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
+ case Thy_Header.THEORY =>
val header =
resources.check_thy_reader("", node_name,
- new CharSequenceReader(span.source), Token.Pos.command)
+ new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
val errors =
for ((imp, pos) <- header.imports if !can_import(imp)) yield {
val msg =
@@ -398,14 +394,6 @@
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
- /* name */
-
- def name: String =
- span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
-
- def position: Position.T =
- span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
-
override def toString: String = id + "/" + span.kind.toString
--- a/src/Pure/PIDE/command_span.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/PIDE/command_span.scala Wed Mar 18 13:31:52 2015 +0100
@@ -26,26 +26,26 @@
sealed case class Span(kind: Kind, content: List[Token])
{
- def length: Int = (0 /: content)(_ + _.source.length)
+ def name: String =
+ kind match { case Command_Span(name, _) => name case _ => "" }
- def source: String =
- content match {
- case List(tok) => tok.source
- case toks => toks.map(_.source).mkString
- }
+ def position: Position.T =
+ kind match { case Command_Span(_, pos) => pos case _ => Position.none }
+
+ def length: Int = (0 /: content)(_ + _.source.length)
def compact_source: (String, Span) =
{
- val src = source
+ val source = Token.implode(content)
val content1 = new mutable.ListBuffer[Token]
var i = 0
for (Token(kind, s) <- content) {
val n = s.length
- val s1 = src.substring(i, i + n)
+ val s1 = source.substring(i, i + n)
content1 += Token(kind, s1)
i += n
}
- (src, Span(kind, content1.toList))
+ (source, Span(kind, content1.toList))
}
}
--- a/src/Pure/PIDE/document.ML Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/PIDE/document.ML Wed Mar 18 13:31:52 2015 +0100
@@ -552,8 +552,7 @@
val initial' = initial andalso
(case prev of
NONE => true
- | SOME command_id =>
- not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
+ | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN);
in (visible', initial') end;
fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
@@ -614,7 +613,7 @@
val exec' = (eval', prints');
val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
- val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
+ val init' = if command_name = Thy_Header.theoryN then NONE else init;
in SOME (assign_update', (command_id', (eval', prints')), init') end;
fun removed_execs node0 (command_id, exec_ids) =
--- a/src/Pure/PIDE/protocol.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/PIDE/protocol.scala Wed Mar 18 13:31:52 2015 +0100
@@ -329,7 +329,7 @@
}
protocol_command("Document.define_command",
- (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
+ (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml ::
toks.map(tok => encode(tok.source))): _*)
}
--- a/src/Pure/PIDE/prover.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/PIDE/prover.scala Wed Mar 18 13:31:52 2015 +0100
@@ -20,7 +20,6 @@
def ++ (other: Syntax): Syntax
def add_keywords(keywords: Thy_Header.Keywords): Syntax
def parse_spans(input: CharSequence): List[Command_Span.Span]
- def is_theory_begin(name: String): Boolean
def load_command(name: String): Option[List[String]]
def load_commands_in(text: String): Boolean
}
--- a/src/Pure/Thy/thy_header.ML Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/Thy/thy_header.ML Wed Mar 18 13:31:52 2015 +0100
@@ -12,6 +12,7 @@
imports: (string * Position.T) list,
keywords: keywords}
val make: string * Position.T -> (string * Position.T) list -> keywords -> header
+ val theoryN: string
val bootstrap_keywords: Keyword.keywords
val add_keywords: keywords -> theory -> theory
val get_keywords: theory -> Keyword.keywords
--- a/src/Pure/Thy/thy_header.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/Thy/thy_header.scala Wed Mar 18 13:31:52 2015 +0100
@@ -60,7 +60,7 @@
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)
- def bootstrap_syntax(): Outer_Syntax =
+ lazy val bootstrap_syntax: Outer_Syntax =
Outer_Syntax.init().add_keywords(bootstrap_header)
--- a/src/Pure/Tools/build.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Pure/Tools/build.scala Wed Mar 18 13:31:52 2015 +0100
@@ -438,7 +438,7 @@
info.parent.map(deps(_)) match {
case None =>
(Set.empty[String], Map.empty[String, Document.Node.Name],
- Thy_Header.bootstrap_syntax())
+ Thy_Header.bootstrap_syntax)
case Some(parent) =>
(parent.loaded_theories, parent.known_theories, parent.syntax)
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Wed Mar 18 13:31:52 2015 +0100
@@ -12,6 +12,7 @@
import isabelle._
import scala.collection.mutable
+import scala.util.parsing.input.CharSequenceReader
import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.Buffer
@@ -78,13 +79,19 @@
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
- Exn.capture {
- PIDE.resources.check_thy_reader("", node_name,
- JEdit_Lib.buffer_reader(buffer), Token.Pos.command)
- } match {
- case Exn.Res(header) => header
- case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
- }
+ Token_Markup.line_token_iterator(
+ Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
+ {
+ case Text.Info(range, tok)
+ if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+ })
+ match {
+ case Some(offset) =>
+ val length = buffer.getLength - offset
+ PIDE.resources.check_thy_reader("", node_name,
+ new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
+ case None => Document.Node.no_header
+ }
}
}
else Document.Node.no_header
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 17 17:45:03 2015 +0000
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 18 13:31:52 2015 +0100
@@ -86,13 +86,15 @@
private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
extends Entry
{
- def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
+ def print: String =
+ Time.print_seconds(timing) + "s theory " + quote(name.theory)
def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
{
- def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.name)
+ def print: String =
+ " " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
def follow(snapshot: Document.Snapshot)
{ PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
}