clarified norm_header/header_edit -- disallow update of loaded theories;

--- a/src/Pure/PIDE/document.scala	Wed Aug 24 15:55:43 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 24 16:27:27 2011 +0200
@@ -54,11 +54,10 @@
     case class Header[A, B](header: Node_Header) extends Edit[A, B]
     case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
-    def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
-        : Header[A, B] =
+    def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
       header match {
-        case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
-        case exn => Header[A, B](exn)
+        case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
+        case exn => exn
       }
 
     val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())

--- a/src/Pure/System/session.scala	Wed Aug 24 15:55:43 2011 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 24 16:27:27 2011 +0200
@@ -159,6 +159,28 @@
 
   val thy_info = new Thy_Info(thy_load)
 
+  def header_edit(name: String, master_dir: String,
+    header: Document.Node_Header): Document.Edit_Text =
+  {
+    def norm_import(s: String): String =
+    {
+      val thy_name = Thy_Header.base_name(s)
+      if (thy_load.is_loaded(thy_name)) thy_name
+      else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+    }
+    def norm_use(s: String): String =
+      file_store.append(master_dir, Path.explode(s))
+
+    val header1: Document.Node_Header =
+      header match {
+        case Exn.Res(Thy_Header(thy_name, _, _))
+        if (thy_load.is_loaded(thy_name)) =>
+          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
+        case _ => Document.Node.norm_header(norm_import, norm_use, header)
+      }
+    (name, Document.Node.Header(header1))
+  }
+
 
   /* actor messages */
 
@@ -210,17 +232,7 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
 
-      def norm_import(s: String): String =
-      {
-        val name = Thy_Header.base_name(s)
-        if (thy_load.is_loaded(name)) name
-        else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
-      }
-      def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
-      val norm_header =
-        Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header)
-
-      val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
+      val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
       val change =
         global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))