# HG changeset patch
# User wenzelm
# Date 926777754 -7200
# Node ID 123b215882aea5d7a292862ae25cb3bda9d3c417
# Parent  ff827fccffb56cb6907b9e537d3a4bd866307c1a
tuned;

diff -r ff827fccffb5 -r 123b215882ae src/Pure/General/README
--- a/src/Pure/General/README	Wed May 12 17:58:03 1999 +0200
+++ b/src/Pure/General/README	Sat May 15 16:15:54 1999 +0200
@@ -14,11 +14,11 @@
   NameSpace     (hierarchically structured name spaces)
   Position      (input positions)
   Scan          (generic scanner toolbox)
+  Source        (co-algebraic data sources)
+  Symbol        (generalized characters)
   Path          (abstract algebra of file paths)
+  Url           (basic URL support)
   File          (file system operations)
   Buffer	(simple string buffers)
   History       (histories of values, with undo and redo)
-  Source        (co-algebraic data sources)
-  Symbol        (generalized characters)
   Pretty        (generic pretty printing module)
-  Use		(enhanced ML 'use' command)
diff -r ff827fccffb5 -r 123b215882ae src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Wed May 12 17:58:03 1999 +0200
+++ b/src/Pure/General/ROOT.ML	Sat May 15 16:15:54 1999 +0200
@@ -29,12 +29,12 @@
   structure NameSpace = NameSpace;
   structure Position = Position;
   structure Scan = Scan;
+  structure Source = Source;
   structure Symbol = Symbol;
   structure Path = Path;
   structure Url = Url;
   structure File = File;
   structure Buffer = Buffer;
   structure History = History;
-  structure Source = Source;
   structure Pretty = Pretty;
 end;
diff -r ff827fccffb5 -r 123b215882ae src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed May 12 17:58:03 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sat May 15 16:15:54 1999 +0200
@@ -38,16 +38,18 @@
 struct
   structure ProofContext = ProofContext;
   structure Proof = Proof;
+  structure ProofHistory = ProofHistory;
   structure Args = Args;
   structure Attrib = Attrib;
   structure Method = Method;
+  structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;
-  structure ProofHistory = ProofHistory;
   structure Toplevel = Toplevel;
-  structure OuterSyntax = OuterSyntax;
+  structure Session = Session;
   structure IsarThy = IsarThy;
   structure IsarCmd = IsarCmd;
+  structure OuterSyntax = OuterSyntax;
   structure IsarSyn = IsarSyn;
   structure Isar = Isar;
 end;
diff -r ff827fccffb5 -r 123b215882ae src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Wed May 12 17:58:03 1999 +0200
+++ b/src/Pure/Isar/isar.ML	Sat May 15 16:15:54 1999 +0200
@@ -7,24 +7,16 @@
 
 signature ISAR =
 sig
-  type parser
   val main: unit -> unit
   val loop: unit -> unit
   val help: unit -> unit
-  val commands: unit -> string list
-  val add_keywords: string list -> unit
-  val add_parsers: parser list -> unit
 end;
 
 structure Isar: ISAR =
 struct
 
-type parser = OuterSyntax.parser;
 val main = OuterSyntax.main;
 val loop = OuterSyntax.loop;
 val help = OuterSyntax.help;
-val commands = OuterSyntax.commands;
-val add_keywords = OuterSyntax.add_keywords;
-val add_parsers = OuterSyntax.add_parsers;
 
 end;