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