| Sun, 22 Mar 2009 20:50:02 +0100 |
wenzelm |
added read_antiq, with improved error reporting;
|
changeset |
files
|
| Sun, 22 Mar 2009 20:49:48 +0100 |
wenzelm |
ML_Lex.read_antiq;
|
changeset |
files
|
| Sun, 22 Mar 2009 20:49:48 +0100 |
wenzelm |
ML_Lex.read_antiq;
|
changeset |
files
|
| Sun, 22 Mar 2009 20:49:47 +0100 |
wenzelm |
simplified Antiquote.read (again);
|
changeset |
files
|
| Sun, 22 Mar 2009 20:49:47 +0100 |
wenzelm |
export report -- version that actually covers all cases;
|
changeset |
files
|
| Sun, 22 Mar 2009 19:12:36 +0100 |
wenzelm |
Test of advanced ML compiler invocation in Poly/ML 5.3.
|
changeset |
files
|
| Sun, 22 Mar 2009 19:11:00 +0100 |
wenzelm |
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
|
changeset |
files
|
| Sun, 22 Mar 2009 19:10:59 +0100 |
wenzelm |
added pretty_ml;
|
changeset |
files
|
| Sun, 22 Mar 2009 19:10:59 +0100 |
wenzelm |
export eval_antiquotes: refined version that operates on ML tokens;
|
changeset |
files
|
| Sun, 22 Mar 2009 19:10:59 +0100 |
wenzelm |
ML_Lex.pos_of: regular position;
|
changeset |
files
|
| Sun, 22 Mar 2009 19:10:58 +0100 |
wenzelm |
replaced Antiquote.is_antiq by Antiquote.is_text;
|
changeset |
files
|
| Sat, 21 Mar 2009 20:39:38 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 21 Mar 2009 20:38:49 +0100 |
wenzelm |
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
|
changeset |
files
|
| Sat, 21 Mar 2009 20:22:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 21 Mar 2009 09:42:55 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 21 Mar 2009 03:24:35 -0700 |
huffman |
move field lemmas into class locale context
|
changeset |
files
|
| Sat, 21 Mar 2009 03:23:17 -0700 |
huffman |
move diff_eq_0_iff_eq into class locale context
|
changeset |
files
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
changeset |
files
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
|
changeset |
files
|
| Sat, 21 Mar 2009 19:58:45 +0100 |
wenzelm |
adapted toplevel_pp to ML_Pretty.pretty;
|
changeset |
files
|
| Sat, 21 Mar 2009 19:58:45 +0100 |
wenzelm |
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
|
changeset |
files
|
| Sat, 21 Mar 2009 19:58:45 +0100 |
wenzelm |
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
|
changeset |
files
|
| Sat, 21 Mar 2009 19:58:44 +0100 |
wenzelm |
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
|
changeset |
files
|
| Sat, 21 Mar 2009 15:09:44 +0100 |
wenzelm |
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
|
changeset |
files
|
| Sat, 21 Mar 2009 15:08:00 +0100 |
wenzelm |
Pretty.position;
|
changeset |
files
|
| Sat, 21 Mar 2009 15:08:00 +0100 |
wenzelm |
added position;
|
changeset |
files
|
| Sat, 21 Mar 2009 15:08:00 +0100 |
wenzelm |
added generic ML_Pretty interface;
|
changeset |
files
|
| Sat, 21 Mar 2009 13:11:12 +0100 |
wenzelm |
restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
|
changeset |
files
|
| Sat, 21 Mar 2009 12:37:13 +0100 |
wenzelm |
more ambitious ML_OPTIONS;
|
changeset |
files
|
| Sat, 21 Mar 2009 12:35:34 +0100 |
wenzelm |
more stats;
|
changeset |
files
|
| Fri, 20 Mar 2009 21:32:12 +0100 |
wenzelm |
added ML syntax markup;
|
changeset |
files
|
| Fri, 20 Mar 2009 20:22:13 +0100 |
wenzelm |
report markup for ML tokens;
|
changeset |
files
|
| Fri, 20 Mar 2009 20:21:38 +0100 |
wenzelm |
Antiquote.read: argument for reporting text;
|
changeset |
files
|
| Fri, 20 Mar 2009 20:20:09 +0100 |
wenzelm |
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
|
changeset |
files
|
| Fri, 20 Mar 2009 20:05:51 +0100 |
wenzelm |
uniform ml_prompts for RAW and Pure;
|
changeset |
files
|
| Fri, 20 Mar 2009 18:46:50 +0100 |
wenzelm |
eliminated old Addsimps;
|
changeset |
files
|
| Fri, 20 Mar 2009 17:12:37 +0100 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
changeset |
files
|
| Fri, 20 Mar 2009 17:04:44 +0100 |
wenzelm |
fixed possibility_tac;
|
changeset |
files
|
| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
changeset |
files
|
| Fri, 20 Mar 2009 11:26:59 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 20 Mar 2009 10:44:25 +0100 |
berghofe |
merged
|
changeset |
files
|
| Fri, 20 Mar 2009 10:43:53 +0100 |
berghofe |
split_codegen now eta-expands terms on-the-fly.
|
changeset |
files
|
| Fri, 20 Mar 2009 11:26:25 +0100 |
wenzelm |
proper context for prove_cont/adm_tac;
|
changeset |
files
|
| Fri, 20 Mar 2009 11:08:59 +0100 |
wenzelm |
with_attributes: canonical capture/release scheme (potentially iron out race condition);
|
changeset |
files
|
| Fri, 20 Mar 2009 09:52:32 +0100 |
wenzelm |
considerable speedup of benchmarks by using minimal simpset;
|
changeset |
files
|
| Fri, 20 Mar 2009 09:51:41 +0100 |
wenzelm |
allow non-printable symbols within string tokens;
|
changeset |
files
|
| Thu, 19 Mar 2009 22:05:37 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 19 Mar 2009 08:13:10 -0700 |
huffman |
add lemma det_diagonal; remove wellorder requirement on several lemmas
|
changeset |
files
|
| Thu, 19 Mar 2009 14:08:55 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 19 Mar 2009 14:08:41 +0100 |
haftmann |
tuned some theorem and attribute bindings
|
changeset |
files
|
| Thu, 19 Mar 2009 22:05:00 +0100 |
wenzelm |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
changeset |
files
|
| Thu, 19 Mar 2009 21:05:40 +0100 |
wenzelm |
eval_antiquotes: joint scanning of ML tokens and antiquotations;
|
changeset |
files
|
| Thu, 19 Mar 2009 21:04:53 +0100 |
wenzelm |
added scan_antiq;
|
changeset |
files
|
| Thu, 19 Mar 2009 19:49:09 +0100 |
wenzelm |
RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);
|
changeset |
files
|
| Thu, 19 Mar 2009 18:20:27 +0100 |
wenzelm |
added tokenize;
|
changeset |
files
|
| Thu, 19 Mar 2009 16:56:51 +0100 |
wenzelm |
parameterized datatype antiquote and read operation;
|
changeset |
files
|
| Thu, 19 Mar 2009 15:44:14 +0100 |
wenzelm |
Antiquote.Text: keep full position information;
|
changeset |
files
|
| Thu, 19 Mar 2009 15:22:53 +0100 |
wenzelm |
OuterLex.read_antiq;
|
changeset |
files
|
| Thu, 19 Mar 2009 15:22:53 +0100 |
wenzelm |
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
|
changeset |
files
|
| Thu, 19 Mar 2009 15:22:53 +0100 |
wenzelm |
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
|
changeset |
files
|