--- 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.
*)
--- 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.
*)
--- 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.
*)
--- 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.
*)
--- 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.
--- 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.
--- 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).
*)
--- 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.
*)
--- 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.
--- 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).
*)
--- 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
--- 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 =
--- 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 =
--- 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 =
--- 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.
*)
--- 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
--- 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;