Skip to content
Success

Changes

Summary

  1. merged
  2. more robust: process stdout on Windows may contain CR;
  3. clarified signature; more inlined protocol messages;
  4. prefer system option: easier to make it default;
  5. support multiple sessions, notably for "isabelle build -P -j2";
  6. pretty formatting as in Isabelle/ML;
  7. output prover messages;
  8. clarified signature;
  9. clarified signature: more robust;
  10. proper parent base;
  11. traditional print_mode for batch build;
  12. proper support for "isabelle build -P Pure";
  13. clarified signature: more robust bootstrap base;
  14. proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
  15. proper context for loading Pure;
  16. clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
  17. close socket explicitly (idempotent);
  18. more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
  19. simplified code and proofs
  20. automated proof
Changeset 71654:0aef1812ae3a by wenzelm:
merged
Changeset 71653:6f7a54954f19 by wenzelm:
more robust: process stdout on Windows may contain CR;
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 71652:721f143a679b by wenzelm:
clarified signature;<br>more inlined protocol messages;
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
Changeset 71651:e26cfcbe20f7 by wenzelm:
prefer system option: easier to make it default;
The file was modified etc/options (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 71650:95ab607398bd by wenzelm:
support multiple sessions, notably for &quot;isabelle build -P -j2&quot;;
The file was modified src/Pure/Tools/simplifier_trace.scala (diff)
The file was modified src/Tools/jEdit/src/simplifier_trace_dockable.scala (diff)
Changeset 71649:2acdbb6ee521 by wenzelm:
pretty formatting as in Isabelle/ML;
The file was modified src/Pure/General/symbol.ML (diff)
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/PIDE/prover.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 71648:12c3fe42b2a8 by wenzelm:
output prover messages;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 71647:7b0656fa783b by wenzelm:
clarified signature;
The file was modified src/Pure/General/output.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
Changeset 71646:86f064893dac by wenzelm:
clarified signature: more robust;
The file was modified src/Pure/System/process_result.scala (diff)
Changeset 71645:07e6053ce89c by wenzelm:
proper parent base;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 71644:60659474ed36 by wenzelm:
traditional print_mode for batch build;
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 71643:43ba9fece20d by wenzelm:
proper support for &quot;isabelle build -P Pure&quot;;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 71642:77327455b00d by wenzelm:
clarified signature: more robust bootstrap base;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 71641:c1409b9c2b22 by wenzelm:
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
The file was modified src/Pure/PIDE/prover.scala (diff)
Changeset 71640:494704309099 by wenzelm:
proper context for loading Pure;
The file was modified src/Pure/System/isabelle_process.ML (diff)
Changeset 71639:ec84f542e411 by wenzelm:
clarified signature of ML_Process vs. Isabelle_Process: proper support for &quot;isabelle build -P -b&quot;;
The file was modified src/Pure/ML/ml_process.scala (diff)
The file was modified src/Pure/System/isabelle_process.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 71638:ec14ef6dd09b by wenzelm:
close socket explicitly (idempotent);
The file was modified src/Pure/System/isabelle_process.ML (diff)
Changeset 71637:45c2b8cf1b26 by wenzelm:
more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
The file was modified src/Pure/General/output.ML (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
Changeset 71636:9d8fb1dbc368 by nipkow:
simplified code and proofs
The file was modified src/HOL/Data_Structures/AVL_Map.thy (diff)
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)
Changeset 71635:b36f07d28867 by nipkow:
automated proof
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)