# HG changeset patch
# User boehmes
# Date 1251811282 -7200
# Node ID 6341f907aba4c202c4ed663520a915ddcb634755
# Parent  7b92a8b8daaf832ae83872fe0bbdee8e810224c4# Parent  6dd577396ed85546fd3fd8441259d728803578d5
merged

diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Tue Sep 01 15:21:22 2009 +0200
@@ -15,7 +15,7 @@
   val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
 end;
 
-structure IsarDocument: ISAR_DOCUMENT =
+structure Isar_Document: ISAR_DOCUMENT =
 struct
 
 (* unique identifiers *)
diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala	Tue Sep 01 15:21:22 2009 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-object IsarDocument
+object Isar_Document
 {
   /* unique identifiers */
 
@@ -17,9 +17,9 @@
 }
 
 
-trait IsarDocument extends Isabelle_Process
+trait Isar_Document extends Isabelle_Process
 {
-  import IsarDocument._
+  import Isar_Document._
 
 
   /* commands */
diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 01 15:21:22 2009 +0200
@@ -30,7 +30,7 @@
 
 val _ =
   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
-    (ThyHeader.args >> (Toplevel.print oo IsarCmd.init_theory));
+    (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
 
 val _ =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Sep 01 15:21:22 2009 +0200
@@ -20,7 +20,7 @@
 fun badcmd text = [D.Badcmd {text = text}];
 
 fun thy_begin text =
-  (case try (ThyHeader.read Position.none) (Source.of_string text) of
+  (case try (Thy_Header.read Position.none) (Source.of_string text) of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
   | SOME (name, imports, _) =>
        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Sep 01 15:21:22 2009 +0200
@@ -11,7 +11,7 @@
   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
 end;
 
-structure ThyHeader: THY_HEADER =
+structure Thy_Header: THY_HEADER =
 struct
 
 structure T = OuterLex;
diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Sep 01 15:21:22 2009 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-object ThyHeader
+object Thy_Header
 {
   val HEADER = "header"
   val THEORY = "theory"
diff -r 7b92a8b8daaf -r 6341f907aba4 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Sep 01 15:20:21 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Sep 01 15:21:22 2009 +0200
@@ -109,7 +109,7 @@
     val master as (path, _) = check_thy dir name;
     val text = explode (File.read path);
     val (name', imports, uses) =
-      ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
+      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
     val _ = check_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;