Unfortunately this sort of thing is a real struggle for Emacs, especially XEmacs (try typing "yes" in a shell buffer of an XEmacs you don't care about...). Suggest you turn off decoration and if you're using XEmacs, switch.

 - D.

On 17/12/10 13:59, Michael Chan wrote:
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.

Reply via email to