--- a/src/Pure/Isar/isar_output.ML Mon Aug 29 16:18:04 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Mon Aug 29 16:18:06 2005 +0200
@@ -206,23 +206,23 @@
(* command spans *)
type command = string * Position.T * string list; (*name, position, tags*)
-type tok = string * token * int; (*raw text, token, meta-comment depth*)
-type source = tok list;
+type tok = token * string * int; (*token, markup flag, meta-comment depth*)
+type source = tok list;
datatype span = Span of command * (source * source * source * source) * bool;
fun make_span cmd src =
let
fun take_newline ((tok: tok) :: toks) =
- if newline_token (#2 tok) then ([tok], toks, true)
+ if newline_token (#1 tok) then ([tok], toks, true)
else ([], tok :: toks, false)
| take_newline [] = ([], [], false);
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
src
- |> take_prefix (improper_token o #2)
- ||>> take_suffix (improper_token o #2)
- ||>> take_prefix (comment_token o #2)
- ||> take_newline;
+ |> take_prefix (improper_token o #1)
+ ||>> take_suffix (improper_token o #1)
+ ||>> take_prefix (comment_token o #1)
+ ||> take_newline;
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
@@ -246,8 +246,8 @@
fun present_span lex default_tags span state state'
(tag_stack, active_tag, newline, buffer, present_cont) =
let
- val present = fold (fn (raw, tok, d) =>
- Buffer.add raw o (if d > 0 then I else Buffer.add (output_token lex state' tok)));
+ val present = fold (fn (tok, flag, 0) =>
+ Buffer.add (output_token lex state' tok) #> Buffer.add flag | _ => I);
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
@@ -329,51 +329,51 @@
(* tokens *)
val ignored = Scan.state --| ignore
- >> (fn d => (NONE, ("", NoToken, d)));
+ >> (fn d => (NONE, (NoToken, "", d)));
- fun markup flag mark mk = Scan.peek (fn d =>
+ fun markup mark mk flag = Scan.peek (fn d =>
improper |--
P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
Scan.repeat tag --
P.!!!! (improper |-- P.position P.text --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
let val name = T.val_of tok
- in (SOME (name, pos, tags), (flag, mk (name, txt), d)) end));
+ in (SOME (name, pos, tags), (mk (name, txt), flag, d)) end));
val command = Scan.peek (fn d =>
P.position (Scan.one (T.is_kind T.Command)) --
Scan.repeat tag
>> (fn ((tok, pos), tags) =>
let val name = T.val_of tok
- in (SOME (name, pos, tags), (Latex.markup_false, BasicToken tok, d)) end));
+ in (SOME (name, pos, tags), (BasicToken tok, Latex.markup_false, d)) end));
val cmt = Scan.peek (fn d =>
P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
- >> (fn txt => (NONE, ("", MarkupToken ("cmt", txt), d))));
+ >> (fn txt => (NONE, (MarkupToken ("cmt", txt), "", d))));
val other = Scan.peek (fn d =>
- Scan.one T.not_eof >> (fn tok => (NONE, ("", BasicToken tok, d))));
+ Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, "", d))));
val token =
ignored ||
- markup Latex.markup_true Markup MarkupToken ||
- markup Latex.markup_true MarkupEnv MarkupEnvToken ||
- markup "" Verbatim (VerbatimToken o #2) ||
+ markup Markup MarkupToken Latex.markup_true ||
+ markup MarkupEnv MarkupEnvToken Latex.markup_true ||
+ markup Verbatim (VerbatimToken o #2) "" ||
command || cmt || other;
(* spans *)
val stopper =
- ((NONE, ("", BasicToken (#1 T.stopper), 0)),
- fn (_, (_, BasicToken x, _)) => #2 T.stopper x | _ => false);
+ ((NONE, (BasicToken (#1 T.stopper), "", 0)),
+ fn (_, (BasicToken x, _, _)) => #2 T.stopper x | _ => false);
val cmd = Scan.one (is_some o #1);
val non_cmd = Scan.one (is_none o #1 andf not o #2 stopper) >> #2;
- val comments = Scan.any (comment_token o #2 o #2);
- val blank = Scan.one (blank_token o #2 o #2);
- val newline = Scan.one (newline_token o #2 o #2);
+ val comments = Scan.any (comment_token o #1 o #2);
+ val blank = Scan.one (blank_token o #1 o #2);
+ val newline = Scan.one (newline_token o #1 o #2);
val before_cmd =
Scan.option (newline -- comments) --
Scan.option (newline -- comments) --