# HG changeset patch
# User wenzelm
# Date 1184102993 -7200
# Node ID 2ebecff57b178a32f054020123bb0d6a7968c641
# Parent  1f84af8b2e719dafe744860a5ce7260c8aada97a
Basic editing of theory sources.

diff -r 1f84af8b2e71 -r 2ebecff57b17 src/Pure/Thy/thy_edit.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_edit.ML	Tue Jul 10 23:29:53 2007 +0200
@@ -0,0 +1,112 @@
+(*  Title:      Pure/Thy/thy_edit.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Basic editing of theory sources.
+*)
+
+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 present_html: Path.T -> Path.T -> unit
+end;
+
+structure ThyEdit: THY_EDIT =
+struct
+
+structure T = OuterLex;
+structure P = OuterParse;
+
+
+(* tokens *)
+
+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);
+
+
+(* 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 *)
+
+local
+
+val token_kind_markup =
+ fn T.Command     => (Markup.commandN, [])
+  | T.Keyword     => (Markup.keywordN, [])
+  | T.Ident       => Markup.ident
+  | T.LongIdent   => Markup.ident
+  | T.SymIdent    => Markup.ident
+  | T.Var         => Markup.ident
+  | T.TypeIdent   => Markup.ident
+  | T.TypeVar     => Markup.ident
+  | T.Nat         => Markup.ident
+  | T.String      => Markup.string
+  | T.AltString   => Markup.altstring
+  | T.Verbatim    => Markup.verbatim
+  | T.Space       => Markup.space
+  | T.Comment     => Markup.comment
+  | T.Sync        => Markup.control
+  | T.Malformed _ => Markup.malformed
+  | T.EOF         => Markup.control;
+
+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;
+
+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);
+
+val present_items = implode o map present_item;
+
+in
+
+fun present_html inpath outpath =
+  read_items (Position.path inpath) (Source.of_string (File.read inpath))
+  |> HTML.html_mode present_items
+  |> enclose
+    (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")
+    ("</pre></div>" ^ HTML.end_document)
+  |> File.write outpath;
+
+end
+
+end;