(*  Title:      Pure/General/markup.ML

    ID:         $Id$

    Author:     Makarius

Common markup elements.

*)

signature MARKUP =

sig

  type property = string * string

  type T = string * property list

  val nameN: string

  val kindN: string

  val none: T

  val properties: (string * string) list -> T -> T

  val lineN: string

  val fileN: string

  val positionN: string val position: T

  val indentN: string

  val blockN: string val block: int -> T

  val breakN: string val break: int -> T

  val fbreakN: string val fbreak: T

  val classN: string val class: string -> T

  val tyconN: string val tycon: string -> T

  val constN: string val const: string -> T

  val axiomN: string val axiom: string -> T

  val sortN: string val sort: T

  val typN: string val typ: T

  val termN: string val term: T

  val keywordN: string val keyword: string -> T

  val commandN: string val command: string -> T

  val promptN: string val prompt: T

  val stateN: string val state: T

  val no_stateN: string val no_state: T

  val subgoalN: string val subgoal: T

end;

structure Markup: MARKUP =

struct

(* basic markup *)

type property = string * string;

type T = string * property list;

val none = ("", []);

fun properties more_props ((elem, props): T) =

  (elem, fold_rev (AList.update (op =)) more_props props);

val nameN = "name";

val kindN = "kind";

fun markup elem = (elem, (elem, []): T);

fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);

fun markup_int elem prop = (elem, fn i => (elem, [(prop, string_of_int i)]): T);

(* position *)

val lineN = "line";

val fileN = "file";

val (positionN, position) = markup "position";

(* pretty printing *)

val indentN = "indent";

val (blockN, block) = markup_int "block" indentN;

val widthN = "width";

val (breakN, break) = markup_int "break" widthN;

val (fbreakN, fbreak) = markup "fbreak";

(* logical entities *)

val (classN, class) = markup_string "class" nameN;

val (tyconN, tycon) = markup_string "tycon" nameN;

val (constN, const) = markup_string "const" nameN;

val (axiomN, axiom) = markup_string "axiom" nameN;

(* inner syntax *)

val (sortN, sort) = markup "sort";

val (typN, typ) = markup "typ";

val (termN, term) = markup "term";

(* outer syntax *)

val (keywordN, keyword) = markup_string "keyword" nameN;

val (commandN, command) = markup_string "command" nameN;

(* toplevel *)

val (promptN, prompt) = markup "prompt";

val (stateN, state) = markup "state";

val (no_stateN, no_state) = markup "no_state";

val (subgoalN, subgoal) = markup "subgoal";

end;