Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more scalable;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;
5 months ago, by wenzelm
NEWS: value-oriented Pretty.T;
5 months ago, by wenzelm
proper formal sections;
5 months ago, by wenzelm
tuned signature: more options;
5 months ago, by wenzelm
clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree;
5 months ago, by wenzelm
minor performance tuning;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");
5 months ago, by wenzelm
clarified signature: more explicit type output_ops: default via print_mode;
5 months ago, by wenzelm
discontinued unused global variable (see also following bf465f335e85);
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified modules (see also ea7c2ee8a47a);
5 months ago, by wenzelm
clarified signature: more explicit type "ops";
5 months ago, by wenzelm
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
5 months ago, by wenzelm
more accurate output, following 3f02bc5a5a03;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
misc tuning and clarification;
5 months ago, by wenzelm
proper signature (amending 0f820da558f9);
5 months ago, by wenzelm
more accurate output: observe depth as in "prune" operation;
5 months ago, by wenzelm
clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;
5 months ago, by wenzelm
clarified signature and modules;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified Pretty.T vs. output tree (following Isabelle/Scala): Output.output_width (via print_mode) happens during formatting, instead of construction;
5 months ago, by wenzelm
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
5 months ago, by wenzelm
clarified signature (see also 8bef51521f21);
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more accurate Default_Metric;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified output_spaces, based on Output.output_width;
5 months ago, by wenzelm
clarified modules: enable pretty.ML to use XML/YXML more directly;
5 months ago, by wenzelm
removed unused operation (reverting 4660b0409096);
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned: prefer Symbol.spaces;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
more NEWS;
5 months ago, by wenzelm
proper string syntax (amending 70076ba563d2);
5 months ago, by wenzelm
avoid redundant XML.blob: Bytes.contents consist of larger chunks;
5 months ago, by wenzelm
minor performance tuning: avoid many small strings, notably in File_Stream.output;
5 months ago, by wenzelm
A bit of tidying
5 months ago, by paulson
merged
5 months ago, by paulson
More tidying of old proofs
5 months ago, by paulson
more scalable pretty printing: avoid exception String.Size at command "value" (line 33 of "$AFP/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy") in AFP/c69af9cd3390;
5 months ago, by wenzelm
more specific "args" syntax, to support more markup for syntax consts;
5 months ago, by wenzelm
more direct notation;
5 months ago, by wenzelm
more specific "args" syntax, to support more markup for syntax consts;
5 months ago, by wenzelm
proper definition to avoid failure of HOL-Codegenerator_Test (amending 3d9e7746d9db);
5 months ago, by wenzelm
further attempts at markup for monad notation;
5 months ago, by wenzelm
more markup for syntax consts;
5 months ago, by wenzelm
stop web server on close;
5 months ago, by Fabian Huch
better results for terminated jobs;
5 months ago, by Fabian Huch
more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;
5 months ago, by Fabian Huch
manage runner state properly (amending be4c1fbccfe8);
5 months ago, by Fabian Huch
merged
5 months ago, by paulson
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
tip