# HG changeset patch
# User wenzelm
# Date 926520748 -7200
# Node ID d2e8342bf5c34f8b1c910adc6f8ee8729ff4979d
# Parent  d399db16964ce486cdb1d7bb163c12143718eb81
rearranged order of modules;

diff -r d399db16964c -r d2e8342bf5c3 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed May 12 16:51:52 1999 +0200
+++ b/src/Pure/General/file.ML	Wed May 12 16:52:28 1999 +0200
@@ -9,7 +9,6 @@
 sig
   val sys_pack_fn: (Path.T -> string) ref
   val sys_unpack_fn: (string -> Path.T) ref
-  val use: Path.T -> unit
   val rm: Path.T -> unit
   val cd: Path.T -> unit
   val pwd: unit -> Path.T
@@ -23,6 +22,9 @@
   val info: Path.T -> info option
   val exists: Path.T -> bool
   val mkdir: Path.T -> unit
+  val source: Path.T -> (string, string list) Source.source * Position.T
+  val plain_use: Path.T -> unit
+  val symbol_use: Path.T -> unit
 end;
 
 structure File: FILE =
@@ -37,8 +39,6 @@
 fun sysify path = ! sys_pack_fn (Path.expand path);
 fun unsysify s = ! sys_unpack_fn s;
 
-
-val use = use o sysify;
 val rm = OS.FileSys.remove o sysify;
 
 
@@ -93,4 +93,34 @@
 fun mkdir path = (execute ("mkdir -p " ^ enclose "'" "'" (sysify path)); ());
 
 
+(* source *)
+
+fun source raw_path =
+  let val path = Path.expand raw_path
+  in (Source.of_string (read path), Position.line_name 1 (quote (Path.pack path))) end;
+
+
+(* symbol_use *)
+
+val plain_use = use o sysify;
+
+(* version of 'use' with input filtering *)
+
+val symbol_use =
+  if not needs_filtered_use then plain_use	(*ML system (wrongly!) accepts non-ASCII*)
+  else
+    fn path =>
+      let
+        val txt = read path;
+        val txt_out = Symbol.input txt;
+      in
+        if txt = txt_out then plain_use path
+        else
+          let val tmp_path = tmp_path path in
+            write tmp_path txt_out;
+            plain_use tmp_path handle exn => (rm tmp_path; raise exn);
+            rm tmp_path
+          end
+      end;
+
 end;
diff -r d399db16964c -r d2e8342bf5c3 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Wed May 12 16:51:52 1999 +0200
+++ b/src/Pure/General/scan.ML	Wed May 12 16:52:28 1999 +0200
@@ -193,7 +193,6 @@
   | _ => None);
 
 
-
 (* infinite scans -- draining state-based source *)
 
 fun drain def_prmpt get stopper scan ((state, xs), src) =
diff -r d399db16964c -r d2e8342bf5c3 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed May 12 16:51:52 1999 +0200
+++ b/src/Pure/General/source.ML	Wed May 12 16:52:28 1999 +0200
@@ -17,7 +17,6 @@
   val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
   val of_list: 'a list -> ('a, 'a list) source
   val of_string: string -> (string, string list) source
-  val of_file: Path.T -> (string, string list) source * Position.T
   val decorate_prompt_fn: (string -> string) ref
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
   val tty: (string, unit) source
@@ -109,10 +108,6 @@
 fun of_list xs = make_source [] xs default_prompt drain_list;
 val of_string = of_list o explode;
 
-fun of_file raw_path =
-  let val path = Path.expand raw_path
-  in (of_string (File.read path), Position.line_name 1 (quote (Path.pack path))) end;
-
 
 (* stream source *)
 
diff -r d399db16964c -r d2e8342bf5c3 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed May 12 16:51:52 1999 +0200
+++ b/src/Pure/General/symbol.ML	Wed May 12 16:52:28 1999 +0200
@@ -23,11 +23,11 @@
   val length: symbol list -> int
   val beginning: symbol list -> string
   val scan: string list -> symbol * string list
+  val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
   val source: bool -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
   val input: string -> string
-  val use: Path.T -> unit
   val add_mode: string -> (string -> string * real) -> unit
   val output: string -> string
   val output_width: string -> string * real
@@ -231,6 +231,20 @@
 
 
 
+(** scanning though symbols **)
+
+fun scanner msg scan chs =
+  let
+    fun err_msg cs = msg ^ ": " ^ beginning cs;
+    val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan));
+  in
+    (case fin_scan chs of
+      (result, []) => result
+    | (_, rest) => error (err_msg rest))
+  end;
+
+
+
 (** symbol input **)
 
 (* scan *)
@@ -274,26 +288,6 @@
   end;
 
 
-(* version of 'use' with input filtering *)
-
-val use =
-  if not needs_filtered_use then File.use	(*ML system (wrongly!) accepts non-ASCII*)
-  else
-    fn path =>
-      let
-        val txt = File.read path;
-        val txt_out = input txt;
-      in
-        if txt = txt_out then File.use path
-        else
-          let val tmp_path = File.tmp_path path in
-            File.write tmp_path txt_out;
-            File.use tmp_path handle exn => (File.rm tmp_path; raise exn);
-            File.rm tmp_path
-          end
-      end;
-
-
 
 (** symbol output **)