src/Pure/context_position.ML
author wenzelm
Mon, 29 Sep 2008 21:26:26 +0200
changeset 28409 a1feb819b0a2
parent 28405 000dee6d5d80
child 29606 fedb8be05f24
permissions -rw-r--r--
renamed report to report_visible; tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28405
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/context_position.ML
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     4
28409
a1feb819b0a2 renamed report to report_visible;
wenzelm
parents: 28405
diff changeset
     5
Context position visibility flag.
28405
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     6
*)
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     7
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     8
signature CONTEXT_POSITION =
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
     9
sig
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    10
  val is_visible: Proof.context -> bool
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    11
  val set_visible: bool -> Proof.context -> Proof.context
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    12
  val restore_visible: Proof.context -> Proof.context -> Proof.context
28409
a1feb819b0a2 renamed report to report_visible;
wenzelm
parents: 28405
diff changeset
    13
  val report_visible: Proof.context -> Markup.T -> Position.T -> unit
28405
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    14
end;
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    15
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    16
structure ContextPosition: CONTEXT_POSITION =
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    17
struct
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    18
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    19
structure Data = ProofDataFun
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    20
(
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    21
  type T = bool;
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    22
  fun init _ = true;
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    23
);
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    24
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    25
val is_visible = Data.get;
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    26
val set_visible = Data.put;
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    27
val restore_visible = set_visible o is_visible;
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    28
28409
a1feb819b0a2 renamed report to report_visible;
wenzelm
parents: 28405
diff changeset
    29
fun report_visible ctxt markup pos =
28405
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    30
  if is_visible ctxt then Position.report markup pos else ();
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    31
000dee6d5d80 Context position visibility.
wenzelm
parents:
diff changeset
    32
end;