Just to add that I can produce the same behaviour on my other faster
machine using the same number of recursions.
Michael
On 16/12/10 17:19, Michael Chan wrote:
Yes, I have. The buffer in *trace* doesn't get wiped out by warnings,
but term highlighting doesn't seem to be consistent. For example, if I
do 30k traces:
ML {*
val t = @{term "P :: 'a => 'b => 'c"};
fun foo 0 = ()
| foo n =
(t |> Syntax.pretty_term @{context}
|> Pretty.string_of
|> tracing; foo (n-1));
foo 30000
*}
only the last ~500 gets the decorations. Or, if I show a warning before
a tracing:
ML {*
val t = @{term "P :: 'a => 'b => 'c"};
fun foo 0 = ()
| foo n =
(warning "testing1"; t |> Syntax.pretty_term @{context}
|> Pretty.string_of
|> tracing; foo (n-1));
foo 5000
*}
Only around the last ~300 gets proper decorations. It takes even fewer,
if I add a warning after the tracing:
ML {*
val t = @{term "P :: 'a => 'b => 'c"};
fun foo 0 = ()
| foo n =
(warning "test1"; t |> Syntax.pretty_term @{context}
|> Pretty.string_of
|> tracing; warning "test2"; foo (n-1));
foo 2000
*}
I suspect it's the intermittent decoration that's causing such
inconsistency. Sometimes I even have the whole tracing window
highlighted with the free variable decoration. I think something is hung
while some other procedure is running.
I'm running PG 3.7.1.
Michael
Makarius
_______________________________________________
ProofGeneral mailing list
ProofGeneral@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
