1.1 --- a/doc-src/rail.ML Sat Aug 29 10:50:04 2009 +0200
1.2 +++ b/doc-src/rail.ML Sat Aug 29 12:01:25 2009 +0200
1.3 @@ -99,7 +99,7 @@
1.4 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
1.5 |> (if ! ThyOutput.quotes then quote else I)
1.6 |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.7 - else hyper o enclose "\\mbox{\\isa{" "}}")), style)
1.8 + else hyper o enclose "\\mbox{\\isa{" "}}")), style)
1.9 else ("Bad " ^ kind ^ " " ^ name, false)
1.10 end;
1.11 end;
1.12 @@ -147,8 +147,8 @@
1.13 ) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||
1.14 scan_link >> (decode_link ctxt) >>
1.15 (fn (txt, style) =>
1.16 - if style then Special_Identifier(txt)
1.17 - else Identifier(txt))
1.18 + if style then Special_Identifier(txt)
1.19 + else Identifier(txt))
1.20 end;
1.21
1.22 fun scan_anot ctxt =
1.23 @@ -169,12 +169,12 @@
1.24 val text_sq =
1.25 Scan.repeat (
1.26 Scan.one (fn s =>
1.27 - s <> "\n" andalso
1.28 - s <> "\t" andalso
1.29 - s <> "'" andalso
1.30 - s <> "\\" andalso
1.31 - Symbol.is_regular s) ||
1.32 - ($$ "\\" |-- $$ "'")
1.33 + s <> "\n" andalso
1.34 + s <> "\t" andalso
1.35 + s <> "'" andalso
1.36 + s <> "\\" andalso
1.37 + Symbol.is_regular s) ||
1.38 + ($$ "\\" |-- $$ "'")
1.39 ) >> implode
1.40 fun quoted scan = $$ "'" |-- scan --| $$ "'";
1.41 in
1.42 @@ -305,9 +305,9 @@
1.43 parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>
1.44 (fn (body1, body2) =>
1.45 if is_empty body2 then
1.46 - add_body(PLUS, new_empty_body, rev_body body1)
1.47 + add_body(PLUS, new_empty_body, rev_body body1)
1.48 else
1.49 - add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
1.50 + add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
1.51 parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
1.52 (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
1.53 parse_body2e
1.54 @@ -365,36 +365,36 @@
1.55 fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =
1.56 let fun max (x,y) = if x > y then x else y
1.57 fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =
1.58 - Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
1.59 + Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
1.60 fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)
1.61 | pos_bodies_cat (x::xs, ystart, ynext, liste) =
1.62 - if is_kind_of CR x then
1.63 - (case set_body_position(x, ystart, ynext+1) of
1.64 - body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.65 - pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
1.66 - )
1.67 - else
1.68 - (case position_body(x, ystart) of
1.69 - body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.70 - pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
1.71 - )
1.72 + if is_kind_of CR x then
1.73 + (case set_body_position(x, ystart, ynext+1) of
1.74 + body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.75 + pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
1.76 + )
1.77 + else
1.78 + (case position_body(x, ystart) of
1.79 + body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.80 + pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
1.81 + )
1.82 fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)
1.83 | pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =
1.84 - (case position_body(x, ystart) of
1.85 - body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.86 - pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
1.87 - )
1.88 + (case position_body(x, ystart) of
1.89 + body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.90 + pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
1.91 + )
1.92 in
1.93 (case kind of
1.94 CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of
1.95 - (bodiesPos, ynext) =>
1.96 - Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.97 + (bodiesPos, ynext) =>
1.98 + Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.99 | BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
1.100 - (bodiesPos, ynext) =>
1.101 - Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.102 + (bodiesPos, ynext) =>
1.103 + Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.104 | PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
1.105 - (bodiesPos, ynext) =>
1.106 - Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.107 + (bodiesPos, ynext) =>
1.108 + Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.109 | CR => set_body_position(body, ystart, ystart+3)
1.110 | EMPTY => set_body_position(body, ystart, ystart+1)
1.111 | ANNOTE => set_body_position(body, ystart, ystart+1)
1.112 @@ -406,15 +406,15 @@
1.113 fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""
1.114 | format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =
1.115 let fun format_bodies([]) = ""
1.116 - | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
1.117 + | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
1.118 in
1.119 format_bodies(bodies)
1.120 end
1.121 | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
1.122 let fun format_bodies([]) = "\\rail@endbar\n"
1.123 - | format_bodies(x::xs) =
1.124 - "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
1.125 - format_body(x, "") ^ format_bodies(xs)
1.126 + | format_bodies(x::xs) =
1.127 + "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
1.128 + format_body(x, "") ^ format_bodies(xs)
1.129 in
1.130 "\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))
1.131 end