GPLed;
authorwenzelm
Fri May 05 22:02:46 2000 +0200 (2000-05-05 ago)
changeset 8806a202293db3f6
parent 8805 e1c36f2c02c0
child 8807 0046be1769f9
GPLed;
src/Pure/General/buffer.ML
src/Pure/General/file.ML
src/Pure/General/graph.ML
src/Pure/General/history.ML
src/Pure/General/name_space.ML
src/Pure/General/object.ML
src/Pure/General/path.ML
src/Pure/General/position.ML
src/Pure/General/pretty.ML
src/Pure/General/scan.ML
src/Pure/General/seq.ML
src/Pure/General/source.ML
src/Pure/General/symbol.ML
src/Pure/General/table.ML
src/Pure/General/url.ML
src/Pure/library.ML
src/Pure/section_utils.ML
     1.1 --- a/src/Pure/General/buffer.ML	Fri May 05 22:00:17 2000 +0200
     1.2 +++ b/src/Pure/General/buffer.ML	Fri May 05 22:02:46 2000 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  (*  Title:      Pure/General/buffer.ML
     1.5      ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  
     1.9  Simple string buffers.
    1.10  *)
     2.1 --- a/src/Pure/General/file.ML	Fri May 05 22:00:17 2000 +0200
     2.2 +++ b/src/Pure/General/file.ML	Fri May 05 22:02:46 2000 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4  (*  Title:      Pure/General/file.ML
     2.5      ID:         $Id$
     2.6      Author:     Markus Wenzel, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9  File system operations.
    2.10  *)
     3.1 --- a/src/Pure/General/graph.ML	Fri May 05 22:00:17 2000 +0200
     3.2 +++ b/src/Pure/General/graph.ML	Fri May 05 22:02:46 2000 +0200
     3.3 @@ -1,6 +1,7 @@
     3.4  (*  Title:      Pure/General/graph.ML
     3.5      ID:         $Id$
     3.6      Author:     Markus Wenzel, TU Muenchen
     3.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8  
     3.9  Directed graphs.
    3.10  *)
     4.1 --- a/src/Pure/General/history.ML	Fri May 05 22:00:17 2000 +0200
     4.2 +++ b/src/Pure/General/history.ML	Fri May 05 22:02:46 2000 +0200
     4.3 @@ -1,6 +1,7 @@
     4.4  (*  Title:      Pure/General/history.ML
     4.5      ID:         $Id$
     4.6      Author:     Markus Wenzel, TU Muenchen
     4.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.8  
     4.9  Histories of values, with undo and redo, and optional limit.
    4.10  *)
     5.1 --- a/src/Pure/General/name_space.ML	Fri May 05 22:00:17 2000 +0200
     5.2 +++ b/src/Pure/General/name_space.ML	Fri May 05 22:02:46 2000 +0200
     5.3 @@ -1,6 +1,7 @@
     5.4  (*  Title:      Pure/General/name_space.ML
     5.5      ID:         $Id$
     5.6      Author:     Markus Wenzel, TU Muenchen
     5.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.8  
     5.9  Hierarchically structured name spaces.
    5.10  
     6.1 --- a/src/Pure/General/object.ML	Fri May 05 22:00:17 2000 +0200
     6.2 +++ b/src/Pure/General/object.ML	Fri May 05 22:02:46 2000 +0200
     6.3 @@ -1,6 +1,7 @@
     6.4  (*  Title:      Pure/General/object.ML
     6.5      ID:         $Id$
     6.6      Author:     Markus Wenzel, TU Muenchen
     6.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.8  
     6.9  Generic objects of arbitrary type -- fool the ML type system via
    6.10  exception constructors.
     7.1 --- a/src/Pure/General/path.ML	Fri May 05 22:00:17 2000 +0200
     7.2 +++ b/src/Pure/General/path.ML	Fri May 05 22:02:46 2000 +0200
     7.3 @@ -1,6 +1,7 @@
     7.4  (*  Title:      Pure/General/path.ML
     7.5      ID:         $Id$
     7.6      Author:     Markus Wenzel, TU Muenchen
     7.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.8  
     7.9  Abstract algebra of file paths (external encoding Unix-style).
    7.10  *)
     8.1 --- a/src/Pure/General/position.ML	Fri May 05 22:00:17 2000 +0200
     8.2 +++ b/src/Pure/General/position.ML	Fri May 05 22:02:46 2000 +0200
     8.3 @@ -1,6 +1,7 @@
     8.4  (*  Title:      Pure/General/position.ML
     8.5      ID:         $Id$
     8.6      Author:     Markus Wenzel, TU Muenchen
     8.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.8  
     8.9  Input positions.
    8.10  *)
     9.1 --- a/src/Pure/General/pretty.ML	Fri May 05 22:00:17 2000 +0200
     9.2 +++ b/src/Pure/General/pretty.ML	Fri May 05 22:02:46 2000 +0200
     9.3 @@ -1,7 +1,8 @@
     9.4  (*  Title:      Pure/General/pretty.ML
     9.5      ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson
     9.7 -    Copyright   1991  University of Cambridge
     9.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.9 +    Author:	Markus Wenzel, TU Munich
    9.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    9.11  
    9.12  Generic pretty printing module.
    9.13  
    10.1 --- a/src/Pure/General/scan.ML	Fri May 05 22:00:17 2000 +0200
    10.2 +++ b/src/Pure/General/scan.ML	Fri May 05 22:02:46 2000 +0200
    10.3 @@ -1,6 +1,7 @@
    10.4  (*  Title:	Pure/General/scan.ML
    10.5      ID:		$Id$
    10.6      Author:	Markus Wenzel and Tobias Nipkow, TU Muenchen
    10.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    10.8  
    10.9  Generic scanners (for potentially infinite input).
   10.10  *)
    11.1 --- a/src/Pure/General/seq.ML	Fri May 05 22:00:17 2000 +0200
    11.2 +++ b/src/Pure/General/seq.ML	Fri May 05 22:02:46 2000 +0200
    11.3 @@ -1,6 +1,8 @@
    11.4  (*  Title:      Pure/General/seq.ML
    11.5      ID:         $Id$
    11.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Author:   	Markus Wenzel, TU Munich
    11.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    11.9  
   11.10  Unbounded sequences implemented by closures.  RECOMPUTES if sequence
   11.11  is re-inspected.  Memoing, using polymorphic refs, was found to be
    12.1 --- a/src/Pure/General/source.ML	Fri May 05 22:00:17 2000 +0200
    12.2 +++ b/src/Pure/General/source.ML	Fri May 05 22:02:46 2000 +0200
    12.3 @@ -1,8 +1,9 @@
    12.4  (*  Title:      Pure/General/source.ML
    12.5      ID:         $Id$
    12.6      Author:     Markus Wenzel, TU Muenchen
    12.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    12.8  
    12.9 -Coalgebraic data sources.
   12.10 +Coalgebraic data sources -- efficient purely functional input streams.
   12.11  *)
   12.12  
   12.13  signature SOURCE =
    13.1 --- a/src/Pure/General/symbol.ML	Fri May 05 22:00:17 2000 +0200
    13.2 +++ b/src/Pure/General/symbol.ML	Fri May 05 22:02:46 2000 +0200
    13.3 @@ -1,8 +1,9 @@
    13.4  (*  Title:      Pure/General/symbol.ML
    13.5      ID:         $Id$
    13.6      Author:     Markus Wenzel, TU Muenchen
    13.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    13.8  
    13.9 -Generalized characters.
   13.10 +Generalized characters, independent of encoding.
   13.11  *)
   13.12  
   13.13  signature SYMBOL =
    14.1 --- a/src/Pure/General/table.ML	Fri May 05 22:00:17 2000 +0200
    14.2 +++ b/src/Pure/General/table.ML	Fri May 05 22:02:46 2000 +0200
    14.3 @@ -1,9 +1,11 @@
    14.4  (*  Title:      Pure/General/table.ML
    14.5      ID:         $Id$
    14.6      Author:     Markus Wenzel, TU Muenchen
    14.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    14.8  
    14.9 -Generic tables and tables indexed by strings.  No delete operation.
   14.10 -Implemented as balanced 2-3 trees.
   14.11 +Generic tables and tables indexed by strings.  Efficient purely
   14.12 +functional implementation using balanced 2-3 trees.  No delete
   14.13 +operation (may store options instead).
   14.14  *)
   14.15  
   14.16  signature KEY =
    15.1 --- a/src/Pure/General/url.ML	Fri May 05 22:00:17 2000 +0200
    15.2 +++ b/src/Pure/General/url.ML	Fri May 05 22:02:46 2000 +0200
    15.3 @@ -1,6 +1,7 @@
    15.4  (*  Title:      Pure/General/url.ML
    15.5      ID:         $Id$
    15.6      Author:     Markus Wenzel, TU Muenchen
    15.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    15.8  
    15.9  Basic URLs.
   15.10  *)
    16.1 --- a/src/Pure/library.ML	Fri May 05 22:00:17 2000 +0200
    16.2 +++ b/src/Pure/library.ML	Fri May 05 22:02:46 2000 +0200
    16.3 @@ -1,7 +1,8 @@
    16.4  (*  Title:      Pure/library.ML
    16.5      ID:         $Id$
    16.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 -    Copyright   1992  University of Cambridge
    16.8 +    Author:	Markus Wenzel, TU Munich
    16.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   16.10  
   16.11  Basic library: functions, options, pairs, booleans, lists, integers,
   16.12  strings, lists as sets, association lists, generic tables, balanced
    17.1 --- a/src/Pure/section_utils.ML	Fri May 05 22:00:17 2000 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,19 +0,0 @@
    17.4 -
    17.5 -(* FIXME get rid of this!! *)
    17.6 -
    17.7 -
    17.8 -(*Read a term from string "b", with expected type T*)
    17.9 -fun readtm sign T b = 
   17.10 -    read_cterm sign (b,T) |> term_of
   17.11 -    handle ERROR => error ("The error(s) above occurred for " ^ b);
   17.12 -
   17.13 -
   17.14 -(* FIXME broken! *)
   17.15 -
   17.16 -(*Skipping initial blanks, find the first identifier*)
   17.17 -fun scan_to_id s =
   17.18 -    s |> Symbol.explode
   17.19 -    |> Scan.error (Scan.finite Symbol.stopper
   17.20 -      (!! (fn _ => "Expected to find an identifier in " ^ s)
   17.21 -        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
   17.22 -    |> #1;