src/Pure/Thy/document_source.ML

more strict AFP properties;

(*  Title:      Pure/Thy/document_source.ML
    Author:     Makarius

Document source for presentation.
*)

signature DOCUMENT_SOURCE =
sig
  val is_white: Token.T -> bool
  val is_black: Token.T -> bool
  val is_white_comment: Token.T -> bool
  val is_black_comment: Token.T -> bool
  val is_improper: Token.T -> bool
  val improper: Token.T list parser
  val improper_end: Token.T list parser
  val blank_end: Token.T list parser
  val get_tags: Proof.context -> string list
  val update_tags: string -> Proof.context -> Proof.context
  val tags: string list parser
  val annotation: unit parser
end;

structure Document_Source: DOCUMENT_SOURCE =
struct

(* white space and comments *)

(*NB: arranging white space around command spans is a black art*)

val is_white = Token.is_space orf Token.is_informal_comment;
val is_black = not o is_white;

val is_white_comment = Token.is_informal_comment;
val is_black_comment = Token.is_formal_comment;


val space_proper =
  Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;

val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
val improper = Scan.many 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 Token.is_blank));


(* syntactic tags (old-style) *)

structure Tags = Proof_Data
(
  type T = string list;
  fun init _ = [];
);

val get_tags = Tags.get;
val update_tags = Tags.map o update (op =);

val tag_name = Parse.group (fn () => "document tag name") (Parse.short_ident || Parse.string);

val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (tag_name --| blank_end);
val tags = Scan.repeat tag;


(* semantic markers (operation on presentation context) *)

val marker = improper |-- Parse.document_marker --| blank_end;

val annotation = Scan.repeat (tag >> K () || marker >> K ()) >> K ();

end;