# HG changeset patch
# User wenzelm
# Date 1254345375 -7200
# Node ID 24ba50c14ec5912245a2b1ff2f27f0f15387db61
# Parent  a08a2b962a09609882834a2007dfc3ab5a5f1934
actually perform Isar_Document.init on startup;

diff -r a08a2b962a09 -r 24ba50c14ec5 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Wed Sep 30 23:13:18 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Wed Sep 30 23:16:15 2009 +0200
@@ -13,6 +13,7 @@
   val begin_document: document_id -> Path.T -> unit
   val end_document: document_id -> unit
   val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
+  val init: unit -> unit
 end;
 
 structure Isar_Document: ISAR_DOCUMENT =
diff -r a08a2b962a09 -r 24ba50c14ec5 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Sep 30 23:13:18 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 30 23:16:15 2009 +0200
@@ -133,6 +133,7 @@
  (Unsynchronized.change print_mode (update (op =) isabelle_processN);
   setup_channels out |> init_message;
   OuterKeyword.report ();
+  Isar_Document.init ();
   Output.status (Markup.markup Markup.ready "");
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});