src/Pure/Isar/isar_output.ML

 
 
 (* 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;
 
 
 (* present spans *)
 

 in
 
 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;
 
     val (tag, tags) = tag_stack;
     val tag' =

 fun present_thy lex default_tags is_markup trs src =
   let
     (* tokens *)
 
     val ignored = Scan.state --| ignore
-      >> (fn d => (NONE, ("", NoToken, d)));
-
-    fun markup flag mark mk = Scan.peek (fn d =>
+      >> (fn d => (NONE, (NoToken, "", 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) --
       Scan.option (blank -- comments) -- cmd;