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