src/Pure/Thy/document_marker.ML
changeset 70068 b9985133805d
child 70070 be04e9a053a7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 00:21:34 2019 +0100
     1.3 @@ -0,0 +1,64 @@
     1.4 +(*  Title:      Pure/Thy/document_marker.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Document markers: declarations on the presentation context.
     1.8 +*)
     1.9 +
    1.10 +signature DOCUMENT_MARKER =
    1.11 +sig
    1.12 +  type marker = Proof.context -> Proof.context
    1.13 +  val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
    1.14 +  val evaluate: Input.source -> marker
    1.15 +end;
    1.16 +
    1.17 +structure Document_Marker: DOCUMENT_MARKER =
    1.18 +struct
    1.19 +
    1.20 +(* theory data *)
    1.21 +
    1.22 +type marker = Proof.context -> Proof.context;
    1.23 +
    1.24 +structure Markers = Theory_Data
    1.25 +(
    1.26 +  type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
    1.27 +  val empty : T = Name_Space.empty_table "document_marker";
    1.28 +  val extend = I;
    1.29 +  val merge = Name_Space.merge_tables;
    1.30 +);
    1.31 +
    1.32 +val get_markers = Markers.get o Proof_Context.theory_of;
    1.33 +
    1.34 +fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt);
    1.35 +
    1.36 +fun setup name scan body thy =
    1.37 +  let
    1.38 +    fun marker src ctxt =
    1.39 +      let val (x, ctxt') = Token.syntax scan src ctxt
    1.40 +      in body x ctxt' end;
    1.41 +  in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
    1.42 +
    1.43 +
    1.44 +(* evaluate inner syntax *)
    1.45 +
    1.46 +val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;
    1.47 +
    1.48 +fun evaluate input ctxt =
    1.49 +  let
    1.50 +    val pos = Input.pos_of input;
    1.51 +    val _ = Context_Position.report ctxt pos Markup.language_document_marker;
    1.52 +
    1.53 +    val syms = Input.source_explode input;
    1.54 +    val markers =
    1.55 +      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
    1.56 +        SOME res => res
    1.57 +      | NONE => error ("Bad input" ^ Position.here pos));
    1.58 +  in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
    1.59 +
    1.60 +
    1.61 +(* concrete markers *)
    1.62 +
    1.63 +val _ =
    1.64 +  Theory.setup
    1.65 +    (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags);
    1.66 +
    1.67 +end;