# HG changeset patch
# User wenzelm
# Date 1426519593 -3600
# Node ID 6410a310fdc2ec77b77bf73b057a09a1b92b9168
# Parent  6c013328b885371f0ba06f49c18f2c4475337c31# Parent  5d0c539537c9eae10e0a55c3ccbdf51e69f6d302
merged

diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/General/completion.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -135,10 +135,31 @@
 
   /** semantic completion **/
 
+  def report_no_completion(pos: Position.T): String =
+    YXML.string_of_tree(Semantic.Info(pos, No_Completion))
+
+  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
+    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
+
   object Semantic
   {
     object Info
     {
+      def apply(pos: Position.T, semantic: Semantic): XML.Elem =
+      {
+        val elem =
+          semantic match {
+            case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
+            case Names(total, names) =>
+              XML.Elem(Markup(Markup.COMPLETION, pos),
+                {
+                  import XML.Encode._
+                  pair(int, list(pair(string, pair(string, string))))(total, names)
+                })
+          }
+        XML.Elem(Markup(Markup.REPORT, pos), List(elem))
+      }
+
       def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
         info.info match {
           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/Isar/token.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -161,6 +161,7 @@
     val start: Pos = new Pos(1, 1, "", "")
     def file(file: String): Pos = new Pos(1, 1, file, "")
     def id(id: String): Pos = new Pos(0, 1, "", id)
+    val command: Pos = id(Markup.COMMAND)
   }
 
   final class Pos private[Token](
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -234,7 +234,7 @@
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
-                  range <- Protocol.message_positions(
+                  range <- Protocol_Message.positions(
                     self_id, command.position, chunk_name, chunk, message)
                 } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
               }
@@ -362,13 +362,15 @@
       case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
         val header =
           resources.check_thy_reader("", node_name,
-            new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
-        val import_errors =
+            new CharSequenceReader(span.source), Token.Pos.command)
+        val errors =
           for ((imp, pos) <- header.imports if !can_import(imp)) yield {
-            val name = imp.node
-            "Bad theory import " + Markup.Path(name).markup(quote(name)) + Position.here(pos)
+            val msg =
+              "Bad theory import " +
+                Markup.Path(imp.node).markup(quote(imp.toString)) + Position.here(pos)
+            Exn.Exn(ERROR(msg)): Command.Blob
           }
-        ((header.errors ::: import_errors).map(msg => Exn.Exn(ERROR(msg)): Command.Blob), -1)
+        (errors, -1)
 
       // auxiliary files
       case _ =>
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Mar 16 16:26:33 2015 +0100
@@ -8,7 +8,7 @@
 signature DOCUMENT =
 sig
   val timing: bool Unsynchronized.ref
-  type node_header = string * Thy_Header.header * string list
+  type node_header = {master: string, header: Thy_Header.header, errors: string list}
   type overlay = Document_ID.command * (string * string list)
   datatype node_edit =
     Edits of (Document_ID.command option * Document_ID.command option) list |
@@ -42,7 +42,8 @@
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
 
-type node_header = string * Thy_Header.header * string list;
+type node_header =
+  {master: string, header: Thy_Header.header, errors: string list};
 
 type perspective =
  {required: bool,  (*required node*)
@@ -74,7 +75,8 @@
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
-val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
+val no_header: node_header =
+  {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
@@ -95,20 +97,16 @@
 
 (* basic components *)
 
-fun master_directory (Node {header = (master, _, _), ...}) =
+fun master_directory (Node {header = {master, ...}, ...}) =
   (case try Url.explode master of
     SOME (Url.File path) => path
   | _ => Path.current);
 
-fun set_header header =
+fun set_header master header errors =
   map_node (fn (_, keywords, perspective, entries, result) =>
-    (header, keywords, perspective, entries, result));
+    ({master = master, header = header, errors = errors}, 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 get_header (Node {header, ...}) = header;
 
 fun set_keywords keywords =
   map_node (fn (header, _, perspective, entries, result) =>
@@ -118,7 +116,16 @@
 
 fun read_header node span =
   let
-    val {name = (name, _), imports, keywords} = #2 (get_header node);
+    val {header, errors, ...} = get_header node;
+    val _ =
+      if null errors then ()
+      else
+        cat_lines errors |>
+        (case Position.get_id (Position.thread_data ()) of
+          NONE => I
+        | SOME id => Protocol_Message.command_positions_yxml id)
+        |> error;
+    val {name = (name, _), imports, keywords} = header;
     val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
   in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
 
@@ -232,7 +239,7 @@
   Version
     (case node_edit of
       Edits edits => update_node name (edit_node edits) nodes
-    | Deps (master, header, errors) =>
+    | Deps {master, header, errors} =>
         let
           val imports = map fst (#imports header);
           val nodes1 = nodes
@@ -244,7 +251,7 @@
           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
+        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 =
@@ -252,7 +259,7 @@
     if is_empty_node node then node
     else
       let
-        val (master, header, errors) = get_header_raw node;
+        val {master, header, errors} = get_header 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);
@@ -262,7 +269,7 @@
               (keywords, if member (op =) errors msg then errors else errors @ [msg]);
       in
         node
-        |> set_header (master, header, errors')
+        |> set_header master header errors'
         |> set_keywords (SOME keywords')
       end);
 
@@ -513,21 +520,29 @@
     val master_dir = master_directory node;
     val header = read_header node span;
     val imports = #imports header;
-    val parents =
-      imports |> map (fn (import, _) =>
+
+    fun maybe_end_theory pos st =
+      SOME (Toplevel.end_theory pos st)
+        handle ERROR msg => (Output.error_message msg; NONE);
+    val parents_reports =
+      imports |> map_filter (fn (import, pos) =>
         (case loaded_theory import of
-          SOME thy => thy
-        | NONE =>
-            Toplevel.end_theory (Position.file_only import)
+          NONE =>
+            maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
                 NONE => Toplevel.toplevel
-              | SOME eval => Command.eval_result_state eval)));
-    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
+              | SOME eval => Command.eval_result_state eval)
+        | some => some)
+        |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
+
+    val parents =
+      if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports;
+    val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 
 fun check_theory full name node =
   is_some (loaded_theory name) orelse
-  can get_header node andalso (not full orelse is_some (get_result node));
+  null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
 
 fun last_common keywords state node_required node0 node =
   let
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Mon Mar 16 16:26:33 2015 +0100
@@ -32,11 +32,15 @@
       let
         val (blobs, blobs_index) =
           YXML.parse_body blobs_yxml |>
-            let open XML.Decode in
+            let
+              val message =
+                YXML.string_of_body o Protocol_Message.command_positions id;
+              open XML.Decode;
+            in
               pair
                 (list (variant
                  [fn ([], a) => Exn.Res (pair string (option string) a),
-                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+                  fn ([], a) => Exn.Exn (ERROR (message a))]))
                 int
             end;
         val toks =
@@ -78,7 +82,7 @@
                               (list YXML.string_of_body)))) a;
                         val imports' = map (rpair Position.none) imports;
                         val header = Thy_Header.make (name, Position.none) imports' keywords;
-                      in Document.Deps (master, header, errors) end,
+                      in Document.Deps {master = master, header = header, errors = errors} end,
                     fn (a :: b, c) =>
                       Document.Perspective (bool_atom a, map int_atom b,
                         list (pair int (pair string (list string))) c)]))
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -186,34 +186,6 @@
 
   /* result messages */
 
-  private val clean_elements =
-    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
-
-  def clean_message(body: XML.Body): XML.Body =
-    body filter {
-      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
-      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
-      case _ => true
-    } map {
-      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
-      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
-      case t => t
-    }
-
-  def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
-    body flatMap {
-      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
-        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
-      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
-        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
-      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
-      case XML.Elem(_, ts) => message_reports(props, ts)
-      case XML.Text(_) => Nil
-    }
-
-
-  /* specific messages */
-
   def is_result(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -302,53 +274,6 @@
         case _ => None
       }
   }
-
-
-  /* reported positions */
-
-  private val position_elements =
-    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-
-  def message_positions(
-    self_id: Document_ID.Generic => Boolean,
-    command_position: Position.T,
-    chunk_name: Symbol.Text_Chunk.Name,
-    chunk: Symbol.Text_Chunk,
-    message: XML.Elem): Set[Text.Range] =
-  {
-    def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
-      props match {
-        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
-          val opt_range =
-            Position.Range.unapply(props) orElse {
-              if (name == Symbol.Text_Chunk.Default)
-                Position.Range.unapply(command_position)
-              else None
-            }
-          opt_range match {
-            case Some(symbol_range) =>
-              chunk.incorporate(symbol_range) match {
-                case Some(range) => set + range
-                case _ => set
-              }
-            case None => set
-          }
-        case _ => set
-      }
-
-    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
-      tree match {
-        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
-          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
-        case XML.Elem(Markup(name, props), body) =>
-          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
-        case XML.Text(_) => set
-      }
-
-    val set = positions(Set.empty, message)
-    if (set.isEmpty) elem_positions(message.markup.properties, set)
-    else set
-  }
 }
 
 
@@ -382,29 +307,6 @@
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
 
-  private def resolve_id(id: String, body: XML.Body): XML.Body =
-  {
-    def resolve_property(p: (String, String)): (String, String) =
-      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
-
-    def resolve_markup(markup: Markup): Markup =
-      Markup(markup.name, markup.properties.map(resolve_property))
-
-    def resolve_tree(t: XML.Tree): XML.Tree =
-      t match {
-        case XML.Wrapped_Elem(markup, ts1, ts2) =>
-          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
-        case XML.Elem(markup, ts) =>
-          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
-        case text => text
-      }
-    body.map(resolve_tree _)
-  }
-
-  private def resolve_id(id: String, s: String): XML.Body =
-    try { resolve_id(id, YXML.parse_body(s)) }
-    catch { case ERROR(_) => XML.Encode.string(s) }
-
   def define_command(command: Command)
   {
     val blobs_yxml =
@@ -413,7 +315,7 @@
         variant(List(
           { case Exn.Res((a, b)) =>
               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
-          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
+          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
       YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/protocol_message.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_message.ML	Mon Mar 16 16:26:33 2015 +0100
@@ -0,0 +1,27 @@
+(*  Title:      Pure/PIDE/protocol_message.ML
+    Author:     Makarius
+
+Auxiliary operations on protocol messages.
+*)
+
+signature PROTOCOL_MESSAGE =
+sig
+  val command_positions: string -> XML.body -> XML.body
+  val command_positions_yxml: string -> string -> string
+end;
+
+structure Protocol_Message: PROTOCOL_MESSAGE =
+struct
+
+fun command_positions id =
+  let
+    fun attribute (a, b) =
+      if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
+    fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
+      | tree text = text;
+  in map tree end;
+
+fun command_positions_yxml id =
+  YXML.string_of_body o command_positions id o YXML.parse_body;
+
+end;
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/protocol_message.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_message.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -0,0 +1,84 @@
+/*  Title:      Pure/PIDE/protocol_message.scala
+    Author:     Makarius
+
+Auxiliary operations on protocol messages.
+*/
+
+package isabelle
+
+
+object Protocol_Message
+{
+  /* inlined reports */
+
+  private val report_elements =
+    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
+
+  def clean_reports(body: XML.Body): XML.Body =
+    body filter {
+      case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
+      case XML.Elem(Markup(name, _), _) => !report_elements(name)
+      case _ => true
+    } map {
+      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
+      case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
+      case t => t
+    }
+
+  def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
+    body flatMap {
+      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
+        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
+      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
+        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
+      case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
+      case XML.Elem(_, ts) => reports(props, ts)
+      case XML.Text(_) => Nil
+    }
+
+
+  /* reported positions */
+
+  private val position_elements =
+    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
+  def positions(
+    self_id: Document_ID.Generic => Boolean,
+    command_position: Position.T,
+    chunk_name: Symbol.Text_Chunk.Name,
+    chunk: Symbol.Text_Chunk,
+    message: XML.Elem): Set[Text.Range] =
+  {
+    def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
+      props match {
+        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
+          val opt_range =
+            Position.Range.unapply(props) orElse {
+              if (name == Symbol.Text_Chunk.Default)
+                Position.Range.unapply(command_position)
+              else None
+            }
+          opt_range match {
+            case Some(symbol_range) =>
+              chunk.incorporate(symbol_range) match {
+                case Some(range) => set + range
+                case _ => set
+              }
+            case None => set
+          }
+        case _ => set
+      }
+    def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
+      t match {
+        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
+          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
+        case XML.Elem(Markup(name, props), body) =>
+          body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
+        case XML.Text(_) => set
+      }
+
+    val set = tree(Set.empty, message)
+    if (set.isEmpty) elem(message.markup.properties, set)
+    else set
+  }
+}
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/prover.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -108,8 +108,8 @@
   {
     if (kind == Markup.INIT) system_channel.accepted()
 
-    val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
-    val reports = Protocol.message_reports(props, body)
+    val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
+    val reports = Protocol_Message.reports(props, body)
     for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   }
 
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/resources.ML	Mon Mar 16 16:26:33 2015 +0100
@@ -68,7 +68,8 @@
     val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
     val _ = thy_name <> name andalso
-      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
+      error ("Bad theory name " ^ quote name ^
+        " for file " ^ Path.print path ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -96,8 +96,9 @@
         val base_name = Long_Name.base_name(node_name.theory)
         val (name, pos) = header.name
         if (base_name != name)
-          error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
-            " for theory " + quote(name) + Position.here(pos))
+          error("Bad theory name " + quote(name) +
+            " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) +
+            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
           header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/ROOT	Mon Mar 16 16:26:33 2015 +0100
@@ -172,6 +172,7 @@
     "PIDE/execution.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
+    "PIDE/protocol_message.ML"
     "PIDE/query_operation.ML"
     "PIDE/resources.ML"
     "PIDE/session.ML"
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/ROOT.ML	Mon Mar 16 16:26:33 2015 +0100
@@ -310,6 +310,7 @@
 use "PIDE/resources.ML";
 use "Thy/thy_info.ML";
 use "PIDE/session.ML";
+use "PIDE/protocol_message.ML";
 use "PIDE/document.ML";
 
 (*theory and proof operations*)
diff -r 6c013328b885 -r 6410a310fdc2 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Pure/build-jars	Mon Mar 16 16:26:33 2015 +0100
@@ -64,6 +64,7 @@
   PIDE/markup.scala
   PIDE/markup_tree.scala
   PIDE/protocol.scala
+  PIDE/protocol_message.scala
   PIDE/prover.scala
   PIDE/query_operation.scala
   PIDE/resources.scala
diff -r 6c013328b885 -r 6410a310fdc2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Mar 16 14:52:34 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Mar 16 16:26:33 2015 +0100
@@ -80,7 +80,7 @@
       JEdit_Lib.buffer_lock(buffer) {
         Exn.capture {
           PIDE.resources.check_thy_reader("", node_name,
-            JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
+            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))