isabelle: Graph

tuned module structure;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
minor performance tuning, following Isabelle/Scala;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
more scalable;
12 months ago, by wenzelm
tuned;
12 months ago, by wenzelm
eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;
12 months ago, by wenzelm
NEWS: value-oriented Pretty.T;
12 months ago, by wenzelm
proper formal sections;
12 months ago, by wenzelm
tuned signature: more options;
12 months ago, by wenzelm
clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree;
12 months ago, by wenzelm
minor performance tuning;
12 months ago, by wenzelm
unused;
12 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");
12 months ago, by wenzelm
clarified signature: more explicit type output_ops: default via print_mode;
12 months ago, by wenzelm
discontinued unused global variable (see also following bf465f335e85);
12 months ago, by wenzelm
tuned signature;
12 months ago, by wenzelm
clarified modules (see also ea7c2ee8a47a);
12 months ago, by wenzelm
clarified signature: more explicit type "ops";
12 months ago, by wenzelm
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
12 months ago, by wenzelm
more accurate output, following 3f02bc5a5a03;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
clarified signature;
12 months ago, by wenzelm
misc tuning and clarification;
12 months ago, by wenzelm
proper signature (amending 0f820da558f9);
12 months ago, by wenzelm
more accurate output: observe depth as in "prune" operation;
12 months ago, by wenzelm
clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;
12 months ago, by wenzelm
clarified signature and modules;
12 months ago, by wenzelm
tuned;
12 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;
12 months ago, by wenzelm
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
12 months ago, by wenzelm
clarified signature (see also 8bef51521f21);
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
more accurate Default_Metric;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
clarified output_spaces, based on Output.output_width;
13 months ago, by wenzelm
clarified modules: enable pretty.ML to use XML/YXML more directly;
13 months ago, by wenzelm
removed unused operation (reverting 4660b0409096);
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer Symbol.spaces;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more NEWS;
13 months ago, by wenzelm
proper string syntax (amending 70076ba563d2);
13 months ago, by wenzelm
avoid redundant XML.blob: Bytes.contents consist of larger chunks;
13 months ago, by wenzelm
minor performance tuning: avoid many small strings, notably in File_Stream.output;
13 months ago, by wenzelm
A bit of tidying
13 months ago, by paulson
merged
13 months ago, by paulson
More tidying of old proofs
13 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;
13 months ago, by wenzelm
more specific "args" syntax, to support more markup for syntax consts;
13 months ago, by wenzelm
more direct notation;
13 months ago, by wenzelm
more specific "args" syntax, to support more markup for syntax consts;
13 months ago, by wenzelm
proper definition to avoid failure of HOL-Codegenerator_Test (amending 3d9e7746d9db);
13 months ago, by wenzelm
further attempts at markup for monad notation;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
stop web server on close;
13 months ago, by Fabian Huch
better results for terminated jobs;
13 months ago, by Fabian Huch
more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;
13 months ago, by Fabian Huch
manage runner state properly (amending be4c1fbccfe8);
13 months ago, by Fabian Huch
merged
13 months ago, by paulson
More tidying of old proofs
13 months ago, by paulson
more precise bound
13 months ago, by nipkow
merged
13 months ago, by nipkow
get rid of manual T_f defs
13 months ago, by nipkow
NEWS and documentation;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
use nicer notation, following 783406dd051e;
13 months ago, by wenzelm
merged
13 months ago, by paulson
A bit more tidying
13 months ago, by paulson
more markup for syntax consts;
13 months ago, by wenzelm
clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;
13 months ago, by wenzelm
use nicer notation, following 783406dd051e;
13 months ago, by wenzelm
proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59);
13 months ago, by wenzelm
tuned: prefer notation for Pure.type;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned, following be8c0e039a5e;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;
13 months ago, by wenzelm
Some tidying
13 months ago, by paulson
merged
13 months ago, by paulson
Tidied some messy old proofs
13 months ago, by paulson
merged
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
more markup for syntax consts;
13 months ago, by wenzelm
clarified concrete syntax;
13 months ago, by wenzelm
more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";
13 months ago, by wenzelm
more concrete syntax and more checks;
13 months ago, by wenzelm
clarified signature: more operations;
13 months ago, by wenzelm
support for syntax const dependencies, with minimal integrity checks;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified markup: more uniform treatment of parse/print phase;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified markup: more uniform;
13 months ago, by wenzelm
tuned signature: separate markup vs. extern;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer configuration options via context;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned signature: more operations;
13 months ago, by wenzelm
tuned comments
13 months ago, by nipkow
merged
13 months ago, by paulson
Partial tidying of old proofs
13 months ago, by paulson
merged
13 months ago, by nipkow
new version of time_fun that works for classes; define T_length automatically now
13 months ago, by nipkow
merged
13 months ago, by paulson
revised/generalised some lemmas
13 months ago, by paulson
remove terminated jobs, even if futures do not complete;
13 months ago, by Fabian Huch
terminate jobs properly;
13 months ago, by Fabian Huch
clarified signature: eliminate clones;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
tuned: more antiquotations;
13 months ago, by wenzelm
misc tuning;
13 months ago, by wenzelm
tuned: eliminate clone (with change of internal exceptions);
13 months ago, by wenzelm