src/Pure/Thy/thy_output.ML

 
 
 (* presentation tokens *)
 
 datatype token =
-    No_Token
+    Ignore_Token
   | Basic_Token of Token.T
   | Markup_Token of string * Input.source
   | Markup_Env_Token of string * Input.source
   | Raw_Token of Input.source;
 

 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
 fun present_token state tok =
   (case tok of
-    No_Token => []
+    Ignore_Token => []
   | Basic_Token tok => output_token state tok
   | Markup_Token (cmd, source) =>
       Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
         (output_text state {markdown = false} source)
   | Markup_Env_Token (cmd, source) =>

 
 
     (* tokens *)
 
     val ignored = Scan.state --| ignore
-      >> (fn d => (NONE, (No_Token, ("", d))));
+      >> (fn d => (NONE, (Ignore_Token, ("", d))));
 
     fun markup pred mk flag = Scan.peek (fn d =>
       improper |--
         Parse.position (Scan.one (fn tok =>
           Token.is_command tok andalso pred keywords (Token.content_of tok))) --