src/Pure/PIDE/sendback.ML
author wenzelm
Thu, 22 Nov 2012 22:21:54 +0100
changeset 50172 1a28109edc6d
parent 50164 77668b522ffe
child 50201 c26369c9eda6
permissions -rw-r--r--
defer interpretation of markup via implicit print mode;

(*  Title:      Pure/PIDE/sendback.ML
    Author:     Makarius

Clickable "sendback" areas within the source text (see also
Tools/jEdit/src/sendback.scala).
*)

signature SENDBACK =
sig
  val make_markup: unit -> Markup.T
  val markup: string -> string
  val markup_implicit: string -> string
end;

structure Sendback: SENDBACK =
struct

fun make_markup () =
  let
    val props =
      (case Position.get_id (Position.thread_data ()) of
        SOME id => [(Isabelle_Markup.idN, id)]
      | NONE => []);
  in Markup.properties props Isabelle_Markup.sendback end;

fun markup s = Markup.markup (make_markup ()) s;

fun markup_implicit s = Markup.markup Isabelle_Markup.sendback s;

end;