# HG changeset patch # User wenzelm # Date 1426681912 -3600 # Node ID e705128d5ffe096ffc013749b97d7a78d856c08e # Parent f41a2f77ab1b84b1827d6f62d2dcc581bbe85a3b# Parent c443ca40ef8dfbe5211f08171ad700f65c47c185 merged diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/Isar/keyword.ML --- 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]; diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/Isar/outer_syntax.scala --- 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 _ => diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/Isar/token.scala --- 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 diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/PIDE/command.scala --- 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 diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/PIDE/command_span.scala --- 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)) } } diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/PIDE/document.ML --- 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) = diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/PIDE/protocol.scala --- 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))): _*) } diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/PIDE/prover.scala --- 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 } diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/Thy/thy_header.ML --- 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 diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/Thy/thy_header.scala --- 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) diff -r f41a2f77ab1b -r e705128d5ffe src/Pure/Tools/build.scala --- 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) } diff -r f41a2f77ab1b -r e705128d5ffe src/Tools/jEdit/src/document_model.scala --- 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 diff -r f41a2f77ab1b -r e705128d5ffe src/Tools/jEdit/src/timing_dockable.scala --- 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)) } }