src/Pure/ProofGeneral/parsing.ML

         | NONE => (* an uncategorized keyword is treated as a theory item (maybe wrong) *)
           (parse_warning ("Uncategorized command found: " ^ name ^ " -- using theoryitem");
            [D.Theoryitem {name=NONE,objtype=NONE,text=str}])
    end
 
+
+(* this would be a lot neater if we could match on toks! *)
 fun markup_comment_whs [] = []
-  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
+  | markup_comment_whs (toks as t::ts) = 
     let
         val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
     in
         if not (null prewhs) then
             D.Whitespace {text=implode (map OuterLex.unparse prewhs)}

          | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
          | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
            let
                (* first proper token after whitespace/litcomment/whitespace is command *)
                val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
-               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
-                                                     | _ => error("proof_general/parse_loop impossible")
+               val (cmdtok,itoks') = 
+		   case cmditoks' of x::xs => (x,xs)
+                                   | _ => error("proof_general/parse_loop impossible")
                val (utoks,itoks'') = match_tokens (toks,itoks',[])
                (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
 
                val str = implode (map OuterLex.unparse (cmdtok::utoks))