1.1 --- a/src/Pure/Thy/document_source.ML	Thu Dec 10 09:16:44 2020 +0100
     1.2 +++ b/src/Pure/Thy/document_source.ML	Thu Dec 10 14:38:32 2020 +0100
     1.3 @@ -90,6 +90,15 @@
     1.4  
     1.5  val tag_scope =
     1.6    Parse.group (fn () => "document tag scope") (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"));
     1.7 +(*//---------------------------- test code: NO @{print} available ------------------------\\* )
     1.8 +fun tag_scope toks =
     1.9 +  let
    1.10 +    val xxx =
    1.11 +      (Parse.group (fn () => "document tag scope") 
    1.12 +      (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"))) toks
    1.13 +    val _ = @{print} {a = "Document_Source.tag_scope", result = xxx}
    1.14 +  in xxx end;
    1.15 +( *\\---------------------------- test code: NO @{print} available ------------------------//*)
    1.16  
    1.17  val tag_name =
    1.18    Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);