1.1 --- a/src/Pure/Thy/thy_edit.ML	Thu Jul 12 00:15:41 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_edit.ML	Thu Jul 12 00:15:42 2007 +0200
     1.3 @@ -7,12 +7,18 @@
     1.4  
     1.5  signature THY_EDIT =
     1.6  sig
     1.7 -  val read_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list
     1.8 -  datatype item =
     1.9 -    Whitespace of OuterLex.token list |
    1.10 -    Junk of OuterLex.token list |
    1.11 -    Commandspan of string * OuterLex.token list
    1.12 -  val read_items: Position.T -> (string, 'a) Source.source -> item list
    1.13 +  val token_source: Position.T -> (string, 'a) Source.source ->
    1.14 +    (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
    1.15 +      Source.source
    1.16 +  val parse_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list
    1.17 +  val present_token: OuterLex.token -> output
    1.18 +  datatype item_kind = Whitespace | Junk | Commandspan of string
    1.19 +  type item = item_kind * OuterLex.token list
    1.20 +  val item_source: Position.T -> (string, 'a) Source.source ->
    1.21 +    (item, (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
    1.22 +      Source.source) Source.source
    1.23 +  val parse_items: Position.T -> (string, 'a) Source.source -> item list
    1.24 +  val present_item: item -> output
    1.25    val present_html: Path.T -> Path.T -> unit
    1.26  end;
    1.27  
    1.28 @@ -23,46 +29,18 @@
    1.29  structure P = OuterParse;
    1.30  
    1.31  
    1.32 -(* tokens *)
    1.33 +(** tokens **)
    1.34 +
    1.35 +(* parse *)
    1.36  
    1.37  fun token_source pos src =
    1.38    Symbol.source true src
    1.39    |> T.source (SOME false) OuterSyntax.get_lexicons pos;
    1.40  
    1.41 -fun read_tokens pos src = Source.exhaust (token_source pos src);
    1.42 +fun parse_tokens pos src = Source.exhaust (token_source pos src);
    1.43  
    1.44  
    1.45 -(* items *)
    1.46 -
    1.47 -datatype item =
    1.48 -  Whitespace of T.token list |
    1.49 -  Junk of T.token list |
    1.50 -  Commandspan of string * T.token list;
    1.51 -
    1.52 -local
    1.53 -
    1.54 -val whitespace = Scan.many1 (T.is_kind T.Space orf T.is_kind T.Comment);
    1.55 -val before_command = Scan.optional whitespace [] -- Scan.ahead P.command;
    1.56 -val body = Scan.repeat1 (Scan.unless before_command P.not_eof);
    1.57 -
    1.58 -val item =
    1.59 -  whitespace >> Whitespace ||
    1.60 -  body >> Junk ||
    1.61 -  before_command -- P.not_eof -- Scan.optional body []
    1.62 -    >> (fn (((ws, name), c), bs) => Commandspan (name, ws @ [c] @ bs));
    1.63 -
    1.64 -in
    1.65 -
    1.66 -fun item_source src = src
    1.67 -  |> Source.source T.stopper (Scan.bulk item) NONE;
    1.68 -
    1.69 -end;
    1.70 -
    1.71 -fun read_items pos src =
    1.72 -  Source.exhaust (item_source (token_source pos src));
    1.73 -
    1.74 -
    1.75 -(* presentation *)
    1.76 +(* present *)
    1.77  
    1.78  local
    1.79  
    1.80 @@ -79,28 +57,70 @@
    1.81    | T.EOF       => Markup.control
    1.82    | _           => Markup.none;
    1.83  
    1.84 +in
    1.85 +
    1.86  fun present_token tok =
    1.87    Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
    1.88  
    1.89 -val present_tokens = implode o map present_token;
    1.90 +end;
    1.91  
    1.92 -fun present_item (Whitespace toks) = Markup.enclose Markup.whitespace (present_tokens toks)
    1.93 -  | present_item (Junk toks) = Markup.enclose Markup.junk (present_tokens toks)
    1.94 -  | present_item (Commandspan (name, toks)) =
    1.95 -      Markup.enclose (Markup.commandspan name) (present_tokens toks);
    1.96  
    1.97 -val present_items = implode o map present_item;
    1.98 +
    1.99 +(** items **)
   1.100 +
   1.101 +datatype item_kind = Whitespace | Junk | Commandspan of string;
   1.102 +type item = item_kind * OuterLex.token list;
   1.103 +
   1.104 +
   1.105 +(* parse *)
   1.106 +
   1.107 +local
   1.108 +
   1.109 +val whitespace = Scan.many1 (T.is_kind T.Space orf T.is_kind T.Comment);
   1.110 +val before_command = Scan.optional whitespace [] -- Scan.ahead P.command;
   1.111 +val body = Scan.repeat1 (Scan.unless before_command P.not_eof);
   1.112 +
   1.113 +val item =
   1.114 +  whitespace >> pair Whitespace ||
   1.115 +  body >> pair Junk ||
   1.116 +  before_command -- P.not_eof -- Scan.optional body []
   1.117 +    >> (fn (((ws, name), c), bs) => (Commandspan name, ws @ [c] @ bs));
   1.118  
   1.119  in
   1.120  
   1.121 +fun item_source pos src =
   1.122 +  token_source pos src
   1.123 +  |> Source.source T.stopper (Scan.bulk item) NONE;
   1.124 +
   1.125 +end;
   1.126 +
   1.127 +fun parse_items pos src = Source.exhaust (item_source pos src);
   1.128 +
   1.129 +
   1.130 +(* present *)
   1.131 +
   1.132 +local
   1.133 +
   1.134 +fun item_kind_markup Whitespace = Markup.whitespace
   1.135 +  | item_kind_markup Junk = Markup.junk
   1.136 +  | item_kind_markup (Commandspan name) = Markup.commandspan name;
   1.137 +
   1.138 +in
   1.139 +
   1.140 +fun present_item (kind, toks) =
   1.141 +  Markup.enclose (item_kind_markup kind) (implode (map present_token toks));
   1.142 +
   1.143 +end;
   1.144 +
   1.145 +
   1.146 +(* HTML presentation -- example *)
   1.147 +
   1.148  fun present_html inpath outpath =
   1.149 -  read_items (Position.path inpath) (Source.of_string (File.read inpath))
   1.150 -  |> HTML.html_mode present_items
   1.151 +  Source.exhaust (item_source (Position.path inpath) (Source.of_string (File.read inpath)))
   1.152 +  |> HTML.html_mode (implode o map present_item)
   1.153    |> enclose
   1.154      (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")
   1.155      ("</pre></div>" ^ HTML.end_document)
   1.156    |> File.write outpath;
   1.157  
   1.158 -end
   1.159 -
   1.160  end;