doc-src/rail.ML
author haftmann
Tue, 13 Jul 2010 11:38:04 +0200
changeset 37788 261c61fabc98
parent 37216 3165bc303f66
child 37982 111ce9651564
permissions -rw-r--r--
corrected title
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     1
(*  Title:      doc-src/rail.ML
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     2
    Author:     Michael Kerscher, TUM
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     3
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     4
Railroad diagrams for LaTeX.
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     5
*)
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     6
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     7
structure Rail =
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     8
struct
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
     9
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    10
datatype token =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    11
  Identifier of string |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    12
  Special_Identifier of string |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    13
  Text of string |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    14
  Anot of string |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    15
  Symbol of string |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    16
  EOF;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    17
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    18
fun is_identifier (Identifier _) = true
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    19
  | is_identifier (Special_Identifier _ ) = true
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    20
  | is_identifier _ = false;
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
    21
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    22
fun is_text (Text _) = true
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    23
  | is_text _ = false;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    24
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    25
fun is_anot (Anot _) = true
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    26
  | is_anot _ = false;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    27
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    28
fun is_symbol (Symbol _) = true
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    29
  | is_symbol _ = false;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    30
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    31
fun is_ str = (fn s => s = Symbol str);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    32
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    33
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    34
local (* copied from antiquote-setup... *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    35
fun translate f = Symbol.explode #> map f #> implode;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    36
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    37
fun clean_name "\<dots>" = "dots"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    38
  | clean_name ".." = "ddot"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    39
  | clean_name "." = "dot"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    40
  | clean_name "_" = "underscore"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    41
  | clean_name "{" = "braceleft"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    42
  | clean_name "}" = "braceright"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    43
  | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    44
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    45
fun no_check _ _ = true;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    46
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    47
fun false_check _ _ = false;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    48
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    49
fun thy_check intern defined ctxt =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    50
  let val thy = ProofContext.theory_of ctxt
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    51
  in defined thy o intern thy end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    52
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    53
fun check_tool name =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    54
  File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    55
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    56
val arg = enclose "{" "}";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    57
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    58
val markup_table =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    59
(*  [(kind, (markup, check, style))*)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    60
  Symtab.make [
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    61
  ("syntax", ("", no_check, true)),
36973
b0033a307d1f prefer structure Keyword and Parse;
wenzelm
parents: 32449
diff changeset
    62
  ("command", ("isacommand", K (is_some o Keyword.command_keyword), true)),
b0033a307d1f prefer structure Keyword and Parse;
wenzelm
parents: 32449
diff changeset
    63
  ("keyword", ("isakeyword", K Keyword.is_keyword, true)),
b0033a307d1f prefer structure Keyword and Parse;
wenzelm
parents: 32449
diff changeset
    64
  ("element", ("isakeyword", K Keyword.is_keyword, true)),
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    65
  ("method", ("", thy_check Method.intern Method.defined, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    66
  ("attribute", ("", thy_check Attrib.intern Attrib.defined, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    67
  ("fact", ("", no_check, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    68
  ("variable", ("", no_check, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    69
  ("case", ("", no_check, true)),
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36973
diff changeset
    70
  ("antiquotation", ("", K Thy_Output.defined_command, true)),
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36973
diff changeset
    71
  ("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *)
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    72
  ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    73
  ("inference", ("", no_check, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    74
  ("executable", ("isatt", no_check, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    75
  ("tool", ("isatt", K check_tool, true)),
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    76
  ("file", ("isatt", K (File.exists o Path.explode), true)),
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36973
diff changeset
    77
  ("theory", ("", K Thy_Info.known_thy, true))
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    78
  ];
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    79
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    80
in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    81
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    82
fun decode_link ctxt (kind,index,logic,name) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    83
  let
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    84
  val (markup, check, style) = case Symtab.lookup markup_table kind of
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    85
    SOME x => x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    86
  | NONE => ("", false_check, false);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    87
  val hyper_name =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    88
    "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    89
  val hyper =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    90
    enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    91
    index = "def" ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    92
  val idx =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    93
    if index = "" then ""
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    94
    else "\\index" ^ index ^ arg logic ^ arg kind ^ arg name;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    95
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    96
  if check ctxt name then
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    97
    (idx ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    98
    (Output.output name
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
    99
      |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36973
diff changeset
   100
      |> (if ! Thy_Output.quotes then quote else I)
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36973
diff changeset
   101
      |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   102
          else hyper o enclose "\\mbox{\\isa{" "}}")), style)
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   103
  else ("Bad " ^ kind ^ " " ^ name, false)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   104
  end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   105
end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   106
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   107
val blanks =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   108
  Scan.many Symbol.is_blank >> implode;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   109
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   110
val scan_symbol =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   111
  $$ ";" || $$ ":"|| $$ "("|| $$ ")"|| $$ "+"|| $$ "|"|| $$ "*"|| $$ "?"|| $$ "\\";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   112
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   113
(* escaped version *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   114
val scan_link = (* @{kind{_def|_ref (logic) name} *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   115
  let
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   116
    fun pseudo_antiquote inner_scan = ($$ "@" ^^ $$ "{") |-- inner_scan --| (blanks -- $$ "}");
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   117
    fun parens scan = $$ "(" |-- scan --| $$ ")";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   118
    fun opt_quotes scan = $$ "'" |-- scan --| $$ "'" || scan;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   119
    val letters = Scan.many Symbol.is_letter >> implode;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   120
    val kind_name = letters;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   121
    val opt_kind_type = Scan.optional (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   122
      $$ "_" |-- (Scan.this_string "def" || Scan.this_string "ref")) "";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   123
    val logic_name = letters;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   124
    val escaped_singlequote = $$ "\\" |-- $$ "'";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   125
    val text = Scan.repeat (Scan.one Symbol.is_letter || escaped_singlequote) >> implode;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   126
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   127
   pseudo_antiquote (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   128
    kind_name -- opt_kind_type --
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   129
    (blanks |-- Scan.optional ( parens logic_name ) "") --
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   130
    (blanks |-- opt_quotes text) )
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   131
    >> (fn (((kind,index),logic),name) => (kind, index, logic, name))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   132
end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   133
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   134
(* escaped version *)
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   135
fun scan_identifier ctxt =
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   136
  let fun is_identifier_start s =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   137
    Symbol.is_letter s orelse
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   138
    s = "_"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   139
  fun is_identifier_rest s =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   140
    Symbol.is_letter s orelse
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   141
    Symbol.is_digit s orelse
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   142
    s = "_" orelse
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   143
    s = "."
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   144
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   145
  (Scan.one is_identifier_start :::
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   146
    Scan.repeat (Scan.one is_identifier_rest || ($$ "\\" |-- $$ "'"))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   147
  ) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   148
  scan_link >> (decode_link ctxt) >>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   149
    (fn (txt, style) =>
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   150
        if style then Special_Identifier(txt)
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   151
        else Identifier(txt))
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   152
end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   153
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   154
fun scan_anot ctxt =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   155
  let val scan_anot =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   156
    Scan.many (fn s =>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   157
      s <> "\n" andalso
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   158
      s <> "\t" andalso
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   159
      s <> "]" andalso
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   160
      Symbol.is_regular s) >> implode
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   161
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   162
  $$ "[" |-- scan_link --| $$ "]" >> (fst o (decode_link ctxt)) ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   163
  $$ "[" |-- scan_anot --| $$ "]" >> Output.output
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   164
end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   165
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   166
(* escaped version *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   167
fun scan_text ctxt =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   168
  let
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   169
    val text_sq =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   170
      Scan.repeat (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   171
        Scan.one (fn s =>
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   172
          s <> "\n" andalso
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   173
          s <> "\t" andalso
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   174
          s <> "'" andalso
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   175
          s <> "\\" andalso
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   176
          Symbol.is_regular s) ||
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   177
        ($$ "\\" |-- $$ "'")
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   178
      ) >> implode
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   179
  fun quoted scan = $$ "'" |-- scan --| $$ "'";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   180
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   181
  quoted scan_link >> (fst o (decode_link ctxt)) ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   182
  quoted text_sq >> (enclose "\\isa{" "}" o Output.output)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   183
end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   184
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   185
fun scan_rail ctxt =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   186
  Scan.repeat ( blanks |-- (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   187
    scan_identifier ctxt ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   188
    scan_anot ctxt >> Anot ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   189
    scan_text ctxt >> Text ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   190
    scan_symbol >> Symbol)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   191
  ) --| blanks;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   192
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   193
fun lex_rail txt ctxt = (* Symbol_Pos fuer spaeter durchgereicht *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   194
  Symbol.scanner "Malformed rail-declaration" (scan_rail ctxt) (map fst (Symbol_Pos.explode txt));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   195
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   196
val lex = lex_rail;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   197
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   198
datatype id_kind = UNKNOWN | TOKEN | TERM | NTERM;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   199
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   200
datatype id_type =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   201
  Id of string * id_kind |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   202
  Null_Id;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   203
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   204
datatype body_kind =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   205
  CAT | BAR | PLUS |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   206
  CR | EMPTY | ANNOTE | IDENT | STRING |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   207
  Null_Kind;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   208
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   209
datatype body_type =
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   210
  Body of body_kind * string * string * id_type * body_type list |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   211
  Body_Pos of body_kind * string * string * id_type * body_type list * int * int |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   212
  Empty_Body |
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   213
  Null_Body;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   214
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   215
datatype rule =
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   216
  Rule of id_type * body_type;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   217
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   218
fun new_id id kind = Id (id, kind);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   219
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   220
fun is_empty (Body(kind,_,_,_,_)) = kind = EMPTY;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   221
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   222
fun new_body (kind, Null_Body, Null_Body) = Body (kind, "", "", Null_Id, [])
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   223
  | new_body (kind, body1, body2) = Body (kind, "", "", Null_Id, body1 :: [body2]);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   224
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   225
fun is_kind_of kind (Body(bodyKind,_,_,_,_)) = kind = bodyKind
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   226
  | is_kind_of _ _ = false;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   227
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   228
fun add_list (Body(kind, text, annot, id, bodies), body) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   229
  Body(kind, text, annot, id, bodies @ [body]);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   230
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   231
fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) =
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   232
      Body(kind, text, annot, id, bodies1 @ bodies2);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   233
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   234
fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   235
  if kind = kind1 andalso kind <> BAR then
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   236
    if kind = kind2 then
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   237
      cat_body_lists(body1, body2)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   238
    else (* kind <> kind2 *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   239
      add_list(body1, body2)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   240
  else (* kind <> kind1 orelse kind = BAR *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   241
    if kind = kind2 then
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   242
      cat_body_lists(add_list(new_body(kind,Null_Body,Null_Body), body1), body2)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   243
    else (* kind <> kind2 *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   244
      add_list(add_list(new_body(kind,Null_Body,Null_Body), body1), body2);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   245
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   246
fun rev_body (body as Body (kind, text, annot, id, [])) = body
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   247
  | rev_body (Body (CAT, text, annot, id, bodies)) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   248
      Body(CAT, text, annot, id, map rev_body (rev bodies))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   249
  | rev_body (Body (kind, text, annot, id, bodies)) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   250
      Body(kind, text, annot, id, map rev_body bodies)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   251
  | rev_body body = body;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   252
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   253
fun set_body_text text (Body(k,_,a,i,b)) = Body(k,text,a,i,b);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   254
fun set_body_anot anot (Body(k,t,_,i,b)) = Body(k,t,anot,i,b);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   255
fun set_body_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TOKEN,b);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   256
fun set_body_special_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TERM,b);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   257
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   258
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   259
fun mk_eof _ = EOF;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   260
fun is_eof s = s = EOF;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   261
val stopper = Scan.stopper mk_eof is_eof;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   262
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   263
(* TODO: change this, so the next or next two tokens are printed *)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   264
fun lex_err msg (cs, _) = "rail grammar error: " ^ msg cs;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   265
fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   266
fun $$$ tok = Scan.one (is_ tok);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   267
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   268
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   269
local
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   270
fun new_bar_body([], body2) = body2
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   271
  | new_bar_body(body1::bodies, body2) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   272
      add_body(BAR, body1, new_bar_body(bodies, body2));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   273
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   274
fun new_cat_body(body::[]) = body
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   275
  | new_cat_body(body1::bodies) = add_body(CAT, body1, new_cat_body(bodies));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   276
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   277
fun new_annote_body (Anot anot) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   278
  set_body_text anot (new_body(ANNOTE, Empty_Body, Empty_Body));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   279
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   280
fun new_text_annote_body (Text text, Anot anot) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   281
  set_body_anot anot (set_body_text text (new_body(STRING, Empty_Body, Empty_Body)));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   282
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   283
fun new_ident_body (Identifier ident, Anot anot) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   284
      set_body_anot anot (set_body_ident ident (new_body(IDENT, Empty_Body, Empty_Body)))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   285
  | new_ident_body (Special_Identifier ident, Anot anot) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   286
      set_body_anot anot (set_body_special_ident ident (new_body(IDENT, Empty_Body, Empty_Body)));
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   287
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   288
val new_empty_body = new_body(EMPTY, Null_Body, Null_Body);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   289
in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   290
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   291
fun parse_body x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   292
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   293
  Scan.repeat1 (parse_body0 --| $$$ "|") -- !!! "body0 expected" (parse_body0) >>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   294
    new_bar_body ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   295
  parse_body0
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   296
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   297
and parse_body0 x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   298
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   299
  Scan.one is_anot -- !!! "body1 expected" (parse_body1) >>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   300
    (fn (anot, body) => add_body(CAT, new_annote_body(anot), body))  ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   301
  parse_body1
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   302
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   303
and parse_body1 x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   304
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   305
  parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   306
    (fn (body1, body2) =>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   307
      if is_empty body2 then
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   308
        add_body(PLUS, new_empty_body, rev_body body1)
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   309
      else
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   310
        add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   311
  parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   312
    (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   313
  parse_body2e
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   314
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   315
and parse_body2e x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   316
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   317
  parse_body2 ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   318
  (fn toks => (new_empty_body, toks))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   319
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   320
and parse_body2 x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   321
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   322
  Scan.repeat1 (parse_body3) >> new_cat_body
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   323
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   324
and parse_body3 x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   325
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   326
  parse_body4 --| $$$ "?" >> (fn body => new_body (BAR, new_empty_body, body) ) ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   327
  parse_body4
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   328
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   329
and parse_body4e x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   330
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   331
  parse_body4 ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   332
  (fn toks => (new_empty_body, toks))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   333
  ) x
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   334
and parse_body4 x =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   335
  (
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   336
  $$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   337
  Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   338
    (fn (text, anot) => new_text_annote_body (text,anot)) ||
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   339
  Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   340
    (fn (id, anot) => new_ident_body (id,anot)) ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   341
  $$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   342
  ) x;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   343
end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   344
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   345
fun new_named_rule (Identifier name, body) = Rule(Id(name, UNKNOWN), body)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   346
  | new_named_rule (Special_Identifier name, body) = Rule(Id(name, UNKNOWN), body);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   347
fun new_anonym_rule body = Rule(Null_Id, body);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   348
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   349
val parse_rule =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   350
  (Scan.one (is_identifier) -- ($$$ ":" |-- !!! "body expected" (parse_body)) ) >>
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   351
    new_named_rule ||
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   352
  parse_body >> new_anonym_rule;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   353
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   354
val parse_rules =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   355
  Scan.repeat ( parse_rule --| $$$ ";") @@@ Scan.single parse_rule;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   356
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   357
fun parse_rail s =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   358
  Scan.read stopper parse_rules s;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   359
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   360
val parse = parse_rail;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   361
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   362
fun getystart (Body_Pos(_,_,_,_,_,ystart,_)) = ystart;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   363
fun getynext (Body_Pos(_,_,_,_,_,_,ynext)) = ynext;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   364
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   365
fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   366
  let fun max (x,y) = if x > y then x else y
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   367
    fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   368
          Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   369
    fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   370
      | pos_bodies_cat (x::xs, ystart, ynext, liste) =
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   371
          if is_kind_of CR x then
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   372
              (case set_body_position(x, ystart, ynext+1) of
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   373
                body as Body_Pos(_,_,_,_,_,_,ynext1) =>
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   374
                  pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   375
              )
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   376
          else
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   377
              (case position_body(x, ystart) of
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   378
                body as Body_Pos(_,_,_,_,_,_,ynext1) =>
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   379
                  pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   380
              )
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   381
    fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   382
      | pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   383
          (case position_body(x, ystart) of
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   384
            body as Body_Pos(_,_,_,_,_,_,ynext1) =>
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   385
              pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   386
          )
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   387
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   388
  (case kind of
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   389
    CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   390
              (bodiesPos, ynext) =>
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   391
                Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   392
  | BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   393
              (bodiesPos, ynext) =>
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   394
                Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   395
  | PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   396
              (bodiesPos, ynext) =>
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   397
                Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   398
  | CR => set_body_position(body, ystart, ystart+3)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   399
  | EMPTY => set_body_position(body, ystart, ystart+1)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   400
  | ANNOTE => set_body_position(body, ystart, ystart+1)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   401
  | IDENT => set_body_position(body, ystart, ystart+1)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   402
  | STRING => set_body_position(body, ystart, ystart+1)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   403
  )
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   404
  end;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   405
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   406
fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   407
  | format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   408
    let fun format_bodies([]) = ""
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   409
          | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   410
    in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   411
      format_bodies(bodies)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   412
    end
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   413
  | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   414
    let fun format_bodies([]) = "\\rail@endbar\n"
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   415
          | format_bodies(x::xs) =
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   416
              "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
696d64ed85da eliminated hard tabs;
wenzelm
parents: 32233
diff changeset
   417
              format_body(x, "") ^ format_bodies(xs)
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   418
    in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   419
      "\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   420
    end
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   421
  | format_body (Body_Pos(PLUS,_,_,_,x::y::xs,_,_),cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   422
      "\\rail@plus\n" ^ format_body(x, cent) ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   423
      "\\rail@nextplus{" ^ string_of_int(getystart(y)) ^ "}\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   424
      format_body(y, "c") ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   425
      "\\rail@endplus\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   426
  | format_body (Body_Pos(ANNOTE,text,_,_,_,_,_),cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   427
      "\\rail@annote[" ^ text ^ "]\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   428
  | format_body (Body_Pos(IDENT,_,annot,Id(name,TERM),_,_,_),cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   429
      "\\rail@" ^ cent ^ "token{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   430
  | format_body (Body_Pos(IDENT,_,annot,Id(name,_),_,_,_),cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   431
      "\\rail@" ^ cent ^ "nont{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   432
  | format_body (Body_Pos(CR,_,_,_,_,_,ynext),cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   433
      "\\rail@cr{" ^ string_of_int(ynext) ^ "}\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   434
  | format_body (Body_Pos(STRING,text,annot,_,_,_,_),cent) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   435
      "\\rail@" ^ cent ^ "term{" ^ text ^ "}[" ^ annot ^ "]\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   436
  | format_body _ =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   437
      "\\rail@unknown\n";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   438
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   439
fun out_body (Id(name,_), body) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   440
  let val bodyPos as Body_Pos(_,_,_,_,_,_,ynext) = position_body(body,0)
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   441
  in
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   442
    "\\rail@begin{" ^ string_of_int(ynext) ^ "}{" ^ name ^ "}\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   443
    format_body(bodyPos,"") ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   444
    "\\rail@end\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   445
  end
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   446
  | out_body (Null_Id, body) = out_body (Id("", UNKNOWN), body);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   447
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   448
fun out_rule (Rule(id, body)) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   449
  if is_empty body then ""
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   450
  else out_body (id, body);
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   451
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   452
fun out_rules ([]) = ""
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   453
  | out_rules (rule::rules) = out_rule rule ^ out_rules rules;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   454
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   455
val output_no_rules =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   456
  "\\rail@begin{1}{}\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   457
  "\\rail@setbox{\\bfseries ???}\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   458
  "\\rail@oval\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   459
  "\\rail@end\n";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   460
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   461
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   462
fun print (SOME rules) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   463
    "\\begin{railoutput}\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   464
    out_rules rules ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   465
    "\\end{railoutput}\n"
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   466
  | print (NONE) =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   467
    "\\begin{railoutput}\n" ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   468
    output_no_rules ^
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   469
    "\\end{railoutput}\n";
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   470
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   471
fun process txt ctxt =
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   472
  lex txt ctxt
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   473
  |> parse
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   474
  |> print;
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   475
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36973
diff changeset
   476
val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
32132
29aed5725acb original rail implementation by Michael Kerscher;
wenzelm
parents:
diff changeset
   477
  (fn {context = ctxt,...} => fn txt => process txt ctxt);
32233
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   478
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   479
end;
2b175fc6668a proper header;
wenzelm
parents: 32132
diff changeset
   480