src/Pure/Thy/present.ML
author wenzelm
Sun Oct 03 15:54:25 1999 +0200 (1999-10-03)
changeset 7685 3edd32d588a6
parent 6325 2822885f5e02
child 7727 b52c7d773121
permissions -rw-r--r--
improved theory_source presentation (hook);
wenzelm@6203
     1
(*  Title:      Pure/Thy/present.ML
wenzelm@6203
     2
    ID:         $Id$
wenzelm@6203
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6203
     4
wenzelm@6325
     5
Theory presentation abstract interface.
wenzelm@6203
     6
*)
wenzelm@6203
     7
wenzelm@6203
     8
signature BASIC_PRESENT =
wenzelm@6203
     9
sig
wenzelm@6325
    10
  include BASIC_BROWSER_INFO
wenzelm@6203
    11
end;
wenzelm@6203
    12
wenzelm@6203
    13
signature PRESENT =
wenzelm@6203
    14
sig
wenzelm@6325
    15
  include BROWSER_INFO
wenzelm@7685
    16
  val theory_source_presenter:
wenzelm@7685
    17
    (bool -> string -> (string, string list) Source.source * Position.T -> unit) -> unit
wenzelm@6203
    18
end;
wenzelm@6203
    19
wenzelm@7685
    20
structure Present: PRESENT =
wenzelm@7685
    21
struct
wenzelm@7685
    22
wenzelm@7685
    23
(*mostly fall back on BrowserInfo for the time being*)
wenzelm@7685
    24
open BrowserInfo;
wenzelm@7685
    25
wenzelm@7685
    26
wenzelm@7685
    27
(* theory source presenters *)
wenzelm@7685
    28
wenzelm@7685
    29
local
wenzelm@7685
    30
  val presenters =
wenzelm@7685
    31
    ref ([]: (bool -> string -> (string, string list) Source.source  * Position.T -> unit) list);
wenzelm@7685
    32
in
wenzelm@7685
    33
  fun theory_source_presenter f = presenters := f :: ! presenters;
wenzelm@7685
    34
  fun theory_source is_old name src = seq (fn f => f is_old name src) (! presenters);
wenzelm@7685
    35
end;
wenzelm@7685
    36
wenzelm@7685
    37
wenzelm@7685
    38
end;
wenzelm@7685
    39
wenzelm@7685
    40
Present.theory_source_presenter BrowserInfo.theory_source;
wenzelm@6203
    41
wenzelm@6203
    42
structure BasicPresent: BASIC_PRESENT = Present;
wenzelm@6203
    43
open BasicPresent;