# HG changeset patch
# User wenzelm
# Date 957556966 -7200
# Node ID a202293db3f62e5b156bf814f6e886bf2af071cc
# Parent  e1c36f2c02c02bee5850393b2232297a031e0665
GPLed;

diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/buffer.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/buffer.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Simple string buffers.
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/file.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/file.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 File system operations.
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/graph.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/graph.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Directed graphs.
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/history.ML
--- a/src/Pure/General/history.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/history.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/history.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Histories of values, with undo and redo, and optional limit.
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/name_space.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Hierarchically structured name spaces.
 
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/object.ML
--- a/src/Pure/General/object.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/object.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/object.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Generic objects of arbitrary type -- fool the ML type system via
 exception constructors.
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/path.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/path.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Abstract algebra of file paths (external encoding Unix-style).
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/position.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/position.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Input positions.
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/pretty.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/General/pretty.ML
     ID:         $Id$
-    Author:     Lawrence C Paulson
-    Copyright   1991  University of Cambridge
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:	Markus Wenzel, TU Munich
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Generic pretty printing module.
 
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/scan.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:	Pure/General/scan.ML
     ID:		$Id$
     Author:	Markus Wenzel and Tobias Nipkow, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Generic scanners (for potentially infinite input).
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/seq.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,8 @@
 (*  Title:      Pure/General/seq.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:   	Markus Wenzel, TU Munich
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Unbounded sequences implemented by closures.  RECOMPUTES if sequence
 is re-inspected.  Memoing, using polymorphic refs, was found to be
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/source.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,8 +1,9 @@
 (*  Title:      Pure/General/source.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Coalgebraic data sources.
+Coalgebraic data sources -- efficient purely functional input streams.
 *)
 
 signature SOURCE =
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/symbol.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,8 +1,9 @@
 (*  Title:      Pure/General/symbol.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Generalized characters.
+Generalized characters, independent of encoding.
 *)
 
 signature SYMBOL =
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/table.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,9 +1,11 @@
 (*  Title:      Pure/General/table.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Generic tables and tables indexed by strings.  No delete operation.
-Implemented as balanced 2-3 trees.
+Generic tables and tables indexed by strings.  Efficient purely
+functional implementation using balanced 2-3 trees.  No delete
+operation (may store options instead).
 *)
 
 signature KEY =
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/General/url.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/General/url.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Basic URLs.
 *)
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri May 05 22:00:17 2000 +0200
+++ b/src/Pure/library.ML	Fri May 05 22:02:46 2000 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/library.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    Author:	Markus Wenzel, TU Munich
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Basic library: functions, options, pairs, booleans, lists, integers,
 strings, lists as sets, association lists, generic tables, balanced
diff -r e1c36f2c02c0 -r a202293db3f6 src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Fri May 05 22:00:17 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-
-(* FIXME get rid of this!! *)
-
-
-(*Read a term from string "b", with expected type T*)
-fun readtm sign T b = 
-    read_cterm sign (b,T) |> term_of
-    handle ERROR => error ("The error(s) above occurred for " ^ b);
-
-
-(* FIXME broken! *)
-
-(*Skipping initial blanks, find the first identifier*)
-fun scan_to_id s =
-    s |> Symbol.explode
-    |> Scan.error (Scan.finite Symbol.stopper
-      (!! (fn _ => "Expected to find an identifier in " ^ s)
-        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
-    |> #1;