level: do not account for local theory blocks (relevant for document preparation);
authorwenzelm
Sat Nov 11 21:13:12 2006 +0100 (2006-11-11 ago)
changeset 21310bfcc24fc7c46
parent 21309 367f4512e65c
child 21311 3556301c18cd
level: do not account for local theory blocks (relevant for document preparation);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Nov 11 21:13:11 2006 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Nov 11 21:13:12 2006 +0100
     1.3 @@ -161,10 +161,9 @@
     1.4  fun level (State NONE) = 0
     1.5    | level (State (SOME (node, _))) =
     1.6        (case History.current node of
     1.7 -        Theory (Context.Theory _, _) => 0
     1.8 -      | Theory (Context.Proof _, _) => 1
     1.9 -      | Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1
    1.10 -      | SkipProof (h, _) => History.current h + 2);   (*different notion of proof depth!*)
    1.11 +        Theory _ => 0
    1.12 +      | Proof (prf, _) => Proof.level (ProofHistory.current prf)
    1.13 +      | SkipProof (h, _) => History.current h + 1);   (*different notion of proof depth!*)
    1.14  
    1.15  fun str_of_state (State NONE) = "at top level"
    1.16    | str_of_state (State (SOME (node, _))) =