src/Pure/Thy/thy_load.scala

   def is_ok(str: String): Boolean =
     try { thy_path(Path.explode(str)); true }
     catch { case ERROR(_) => false }
 
 
-  /* node names */
+  /* document node names */
 
-  def external_node(raw_path: Path): Document.Node.Name =
+  def path_node_name(raw_path: Path): Document.Node.Name =
   {
     val path = raw_path.expand
     val node = path.implode
     val dir = path.dir.implode
     val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)

     catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Header =
     with_thy_text(name, check_thy_text(name, _))
+
+
+  /* theory text edits */
+
+  def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
+      : (List[Document.Edit_Command], Document.Version) =
+    Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
 }