src/Pure/Thy/thy_edit.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25)
changeset 27353 71c4dd53d4cb
parent 26881 bb68f50644a9
child 27665 b9e54ba563b3
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
     1 (*  Title:      Pure/Thy/thy_edit.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Basic editing of theory sources.
     6 *)
     7 
     8 signature THY_EDIT =
     9 sig
    10   val token_source: Position.T -> (string, 'a) Source.source ->
    11     (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
    12       Source.source
    13   val parse_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list
    14   val present_token: OuterLex.token -> output
    15   datatype item_kind = Whitespace | Junk | Commandspan of string
    16   type item = item_kind * OuterLex.token list
    17   val item_source: Position.T -> (string, 'a) Source.source ->
    18     (item, (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
    19       Source.source) Source.source
    20   val parse_items: Position.T -> (string, 'a) Source.source -> item list
    21   val present_item: item -> output
    22   val present_html: Path.T -> Path.T -> unit
    23 end;
    24 
    25 structure ThyEdit: THY_EDIT =
    26 struct
    27 
    28 structure T = OuterLex;
    29 structure P = OuterParse;
    30 
    31 
    32 (** tokens **)
    33 
    34 (* parse *)
    35 
    36 fun token_source pos src =
    37   Symbol.source true src
    38   |> T.source (SOME false) OuterKeyword.get_lexicons pos;
    39 
    40 fun parse_tokens pos src = Source.exhaust (token_source pos src);
    41 
    42 
    43 (* present *)
    44 
    45 local
    46 
    47 val token_kind_markup =
    48  fn T.Command   => (Markup.commandN, [])
    49   | T.Keyword   => (Markup.keywordN, [])
    50   | T.String    => Markup.string
    51   | T.AltString => Markup.altstring
    52   | T.Verbatim  => Markup.verbatim
    53   | T.Comment   => Markup.comment
    54   | T.Sync      => Markup.control
    55   | T.Malformed => Markup.malformed
    56   | T.Error _   => Markup.malformed
    57   | T.EOF       => Markup.control
    58   | _           => Markup.none;
    59 
    60 in
    61 
    62 fun present_token tok =
    63   Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
    64 
    65 end;
    66 
    67 
    68 
    69 (** items **)
    70 
    71 datatype item_kind = Whitespace | Junk | Commandspan of string;
    72 type item = item_kind * OuterLex.token list;
    73 
    74 
    75 (* parse *)
    76 
    77 local
    78 
    79 val whitespace = Scan.many1 (T.is_kind T.Space orf T.is_kind T.Comment);
    80 val before_command = Scan.optional whitespace [] -- Scan.ahead P.command;
    81 val body = Scan.repeat1 (Scan.unless before_command P.not_eof);
    82 
    83 val item =
    84   whitespace >> pair Whitespace ||
    85   body >> pair Junk ||
    86   before_command -- P.not_eof -- Scan.optional body []
    87     >> (fn (((ws, name), c), bs) => (Commandspan name, ws @ [c] @ bs));
    88 
    89 in
    90 
    91 fun item_source pos src =
    92   token_source pos src
    93   |> Source.source T.stopper (Scan.bulk item) NONE;
    94 
    95 end;
    96 
    97 fun parse_items pos src = Source.exhaust (item_source pos src);
    98 
    99 
   100 (* present *)
   101 
   102 local
   103 
   104 fun item_kind_markup Whitespace = Markup.whitespace
   105   | item_kind_markup Junk = Markup.junk
   106   | item_kind_markup (Commandspan name) = Markup.commandspan name;
   107 
   108 in
   109 
   110 fun present_item (kind, toks) =
   111   Markup.enclose (item_kind_markup kind) (implode (map present_token toks));
   112 
   113 end;
   114 
   115 
   116 (* HTML presentation -- example *)
   117 
   118 fun present_html inpath outpath =
   119   Source.exhaust (item_source (Path.position inpath) (Source.of_string (File.read inpath)))
   120   |> HTML.html_mode (implode o map present_item)
   121   |> enclose
   122     (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")
   123     ("</pre></div>" ^ HTML.end_document)
   124   |> File.write outpath;
   125 
   126 end;