On 16/12/10 14:51, Makarius wrote:



Did yout try the tracing channel for your messages?


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




--
Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street,
Edinburgh EH8 9AB, UK.
Telephone Number: +44-131-651-3077,
Fax Number: +44-131-650-6899,
Email: m.c...@ed.ac.uk
Web Page: http://homepages.inf.ed.ac.uk/mchan/
_______________________________________________
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