--- 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)
--- 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;
--- 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;
--- 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;