# HG changeset patch
# User wenzelm
# Date 1163275991 -3600
# Node ID 367f4512e65ccbc45398972b4b5a47aca34d6121
# Parent  73883a528b26a4d725c19328444f83a438779e49
local 'end': no default tags;
tag parser: do not swallow trailing newlines;

diff -r 73883a528b26 -r 367f4512e65c src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sat Nov 11 16:12:23 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Sat Nov 11 21:13:11 2006 +0100
@@ -172,6 +172,8 @@
 
 (** present theory source **)
 
+(*NB: arranging white space around command spans is a black art.*)
+
 (* presentation tokens *)
 
 datatype token =
@@ -255,6 +257,7 @@
 
     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');
 
@@ -306,6 +309,7 @@
 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);
 
@@ -316,7 +320,7 @@
     (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") |--