src/Pure/Thy/thy_output.ML

 
 
 
 (** present theory source **)
 
-(*NB: arranging white space around command spans is a black art.*)
+(*NB: arranging white space around command spans is a black art*)
 
 (* presentation tokens *)
 
 datatype token =
     No_Token

       >> (fn (((tok, pos'), tags), source) =>
         let val name = Token.content_of tok
         in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
-      Parse.position (Scan.one (Token.is_command)) --
-      Scan.repeat tag
-      >> (fn ((tok, pos), tags) =>
-        let val name = Token.content_of tok
-        in (SOME (name, pos, tags), (Basic_Token tok, (Latex.markup_false, d))) end));
+      Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
+      Scan.one Token.is_command -- Scan.repeat tag
+      >> (fn ((private, cmd), tags) =>
+        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
+          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
+            (Basic_Token cmd, (Latex.markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>
       Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >>
         (fn source => (NONE, (Markup_Token ("cmt", source), ("", d)))));
 
     val other = Scan.peek (fn d =>
        Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
 
-    val token =
-      ignored ||
-      markup Keyword.is_document_heading Markup_Token Latex.markup_true ||
-      markup Keyword.is_document_body Markup_Env_Token Latex.markup_true ||
-      markup Keyword.is_document_raw (Verbatim_Token o #2) "" ||
-      command || cmt || other;
+    val tokens =
+      (ignored ||
+        markup Keyword.is_document_heading Markup_Token Latex.markup_true ||
+        markup Keyword.is_document_body Markup_Env_Token Latex.markup_true ||
+        markup Keyword.is_document_raw (Verbatim_Token o #2) "") >> single ||
+      command ||
+      (cmt || other) >> single;
 
 
     (* spans *)
 
     val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false;

           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
     val spans = toks
       |> take_suffix Token.is_space |> #1
       |> Source.of_list
-      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token))
+      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
       |> Source.source stopper (Scan.error (Scan.bulk span))
       |> Source.exhaust;
 
 
     (* present commands *)