tuned signature;
misc cleanup / simplification;

--- a/src/Pure/Thy/thy_edit.ML	Thu Jul 12 00:15:41 2007 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Thu Jul 12 00:15:42 2007 +0200
@@ -7,12 +7,18 @@
 
 signature THY_EDIT =
 sig
-  val read_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list
-  datatype item =
-    Whitespace of OuterLex.token list |
-    Junk of OuterLex.token list |
-    Commandspan of string * OuterLex.token list
-  val read_items: Position.T -> (string, 'a) Source.source -> item list
+  val token_source: Position.T -> (string, 'a) Source.source ->
+    (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
+      Source.source
+  val parse_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list
+  val present_token: OuterLex.token -> output
+  datatype item_kind = Whitespace | Junk | Commandspan of string
+  type item = item_kind * OuterLex.token list
+  val item_source: Position.T -> (string, 'a) Source.source ->
+    (item, (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
+      Source.source) Source.source
+  val parse_items: Position.T -> (string, 'a) Source.source -> item list
+  val present_item: item -> output
   val present_html: Path.T -> Path.T -> unit
 end;
 
@@ -23,46 +29,18 @@
 structure P = OuterParse;
 
 
-(* tokens *)
+(** tokens **)
+
+(* parse *)
 
 fun token_source pos src =
   Symbol.source true src
   |> T.source (SOME false) OuterSyntax.get_lexicons pos;
 
-fun read_tokens pos src = Source.exhaust (token_source pos src);
+fun parse_tokens pos src = Source.exhaust (token_source pos src);
 
 
-(* items *)
-
-datatype item =
-  Whitespace of T.token list |
-  Junk of T.token list |
-  Commandspan of string * T.token list;
-
-local
-
-val whitespace = Scan.many1 (T.is_kind T.Space orf T.is_kind T.Comment);
-val before_command = Scan.optional whitespace [] -- Scan.ahead P.command;
-val body = Scan.repeat1 (Scan.unless before_command P.not_eof);
-
-val item =
-  whitespace >> Whitespace ||
-  body >> Junk ||
-  before_command -- P.not_eof -- Scan.optional body []
-    >> (fn (((ws, name), c), bs) => Commandspan (name, ws @ [c] @ bs));
-
-in
-
-fun item_source src = src
-  |> Source.source T.stopper (Scan.bulk item) NONE;
-
-end;
-
-fun read_items pos src =
-  Source.exhaust (item_source (token_source pos src));
-
-
-(* presentation *)
+(* present *)
 
 local
 
@@ -79,28 +57,70 @@
   | T.EOF       => Markup.control
   | _           => Markup.none;
 
+in
+
 fun present_token tok =
   Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
 
-val present_tokens = implode o map present_token;
+end;
+
+
+
+(** items **)
+
+datatype item_kind = Whitespace | Junk | Commandspan of string;
+type item = item_kind * OuterLex.token list;
+
+
+(* parse *)
 
-fun present_item (Whitespace toks) = Markup.enclose Markup.whitespace (present_tokens toks)
-  | present_item (Junk toks) = Markup.enclose Markup.junk (present_tokens toks)
-  | present_item (Commandspan (name, toks)) =
-      Markup.enclose (Markup.commandspan name) (present_tokens toks);
+local
+
+val whitespace = Scan.many1 (T.is_kind T.Space orf T.is_kind T.Comment);
+val before_command = Scan.optional whitespace [] -- Scan.ahead P.command;
+val body = Scan.repeat1 (Scan.unless before_command P.not_eof);
 
-val present_items = implode o map present_item;
+val item =
+  whitespace >> pair Whitespace ||
+  body >> pair Junk ||
+  before_command -- P.not_eof -- Scan.optional body []
+    >> (fn (((ws, name), c), bs) => (Commandspan name, ws @ [c] @ bs));
 
 in
 
+fun item_source pos src =
+  token_source pos src
+  |> Source.source T.stopper (Scan.bulk item) NONE;
+
+end;
+
+fun parse_items pos src = Source.exhaust (item_source pos src);
+
+
+(* present *)
+
+local
+
+fun item_kind_markup Whitespace = Markup.whitespace
+  | item_kind_markup Junk = Markup.junk
+  | item_kind_markup (Commandspan name) = Markup.commandspan name;
+
+in
+
+fun present_item (kind, toks) =
+  Markup.enclose (item_kind_markup kind) (implode (map present_token toks));
+
+end;
+
+
+(* HTML presentation -- example *)
+
 fun present_html inpath outpath =
-  read_items (Position.path inpath) (Source.of_string (File.read inpath))
-  |> HTML.html_mode present_items
+  Source.exhaust (item_source (Position.path inpath) (Source.of_string (File.read inpath)))
+  |> HTML.html_mode (implode o map present_item)
   |> enclose
     (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")
     ("</pre></div>" ^ HTML.end_document)
   |> File.write outpath;
 
-end
-
 end;