src/Pure/Isar/isar_output.ML

 
 
 
 (** present theory source **)
 
+(*NB: arranging white space around command spans is a black art.*)
+
 (* presentation tokens *)
 
 datatype token =
     NoToken
   | BasicToken of T.token

     val (tag, tags) = tag_stack;
     val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
 
     val active_tag' =
       if is_some tag' then tag'
+      else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
       else try hd (default_tags cmd_name);
     val edge = (active_tag, active_tag');
 
     val newline' =
       if is_none active_tag' then span_newline else newline;

   Scan.one T.is_blank -- Scan.any T.is_comment -- Scan.one T.is_proper;
 
 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
 val improper = Scan.any is_improper;
 val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
 
 val opt_newline = Scan.option (Scan.one T.is_newline);
 
 val ignore =
   Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
     >> pair (d + 1)) ||
   Scan.depend (fn d => Scan.one T.is_end_ignore --|
     (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
     >> pair (d - 1));
 
-val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| improper_end);
+val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
 
 val locale =
   Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
     P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));