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