misc tuning and simplification;

--- a/src/Pure/Isar/keyword.ML	Tue Mar 17 09:22:21 2015 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/Isar/token.scala	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/PIDE/prover.scala	Tue Mar 17 15:21:41 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 09:22:21 2015 +0100
+++ b/src/Pure/Thy/thy_header.ML	Tue Mar 17 15:21:41 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/Tools/jEdit/src/timing_dockable.scala	Tue Mar 17 09:22:21 2015 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 17 15:21:41 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)) }
   }