# HG changeset patch # User wenzelm # Date 1279739320 -7200 # Node ID b7ae269c0d68943c4699cb578e05b90920371431 # Parent 4e7864f3643d58d43d2bb36fda199b86b018245e replaced Source.of_list_limited by slightly more economic Source.of_string_limited; diff -r 4e7864f3643d -r b7ae269c0d68 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Wed Jul 21 20:32:08 2010 +0200 +++ b/src/Pure/General/source.ML Wed Jul 21 21:08:40 2010 +0200 @@ -16,9 +16,9 @@ val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source val of_list: 'a list -> ('a, 'a list) source - val of_list_limited: int -> 'a list -> ('a, 'a list) source + val exhausted: ('a, 'b) source -> ('a, 'a list) source val of_string: string -> (string, string list) source - val exhausted: ('a, 'b) source -> ('a, 'a list) source + val of_string_limited: int -> string -> (string, substring) source val tty: (string, unit) source val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option -> @@ -101,11 +101,21 @@ (* list source *) fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, [])); -fun of_list_limited n xs = make_source [] xs default_prompt (fn _ => chop n); + +fun exhausted src = of_list (exhaust src); + + +(* string source *) val of_string = of_list o explode; -fun exhausted src = of_list (exhaust src); +fun of_string_limited limit str = + make_source [] (Substring.full str) default_prompt + (fn _ => fn s => + let + val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit)); + val cs = map String.str (Substring.explode s1); + in (cs, s2) end); (* stream source *) diff -r 4e7864f3643d -r b7ae269c0d68 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Wed Jul 21 20:32:08 2010 +0200 +++ b/src/Pure/Thy/thy_load.ML Wed Jul 21 21:08:40 2010 +0200 @@ -116,7 +116,7 @@ val master as (path, _) = check_thy dir name; val text = File.read path; val (name', imports, uses) = - Thy_Header.read (Path.position path) (Source.of_list_limited 8000 (explode text)); + Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text); val _ = check_name name name'; val uses = map (Path.explode o #1) uses; in {master = master, text = text, imports = imports, uses = uses} end;