2008-08-09 wenzelm 2008-08-09 read_token: more robust handling of empty text;
2008-08-09 wenzelm 2008-08-09 datatype token: maintain range, tuned representation; moved eof, stopper to lexicon.ML;
2008-08-09 wenzelm 2008-08-09 datatype token: maintain range, tuned representation; tuned messages;
2008-08-09 wenzelm 2008-08-09 datatype token: maintain range, tuned representation; added eof, stopper (from simple_parse.ML); str_of_token: no special case for EOF; misc tuning;
2008-08-09 wenzelm 2008-08-09 tuned SymbolPos interface;
2008-08-09 wenzelm 2008-08-09 YXML.parse: allow text without markup, potentially empty;
2008-08-09 wenzelm 2008-08-09 added content; simplified implode: interface and permissive padding via Position.distance_of; added range; renamed implode_delim to implode_range;
2008-08-09 wenzelm 2008-08-09 added distance_of (permissive version); added no_range; tuned;
2008-08-08 wenzelm 2008-08-08 count offset as well; more uniform treatment of invalid fields; tuned;
2008-08-08 wenzelm 2008-08-08 added offset/end_offset;
2008-08-08 wenzelm 2008-08-08 tuned formatting;
2008-08-08 krauss 2008-08-08 clean up dead code
2008-08-08 wenzelm 2008-08-08 made SML/NJ happy;
2008-08-08 krauss 2008-08-08 FundefLib.try_proof : attempt a proof and see if it works
2008-08-08 nipkow 2008-08-08 added lemmas
2008-08-07 wenzelm 2008-08-07 inner_syntax markup is back;
2008-08-07 wenzelm 2008-08-07 disabled inner_syntax markup for now;
2008-08-07 wenzelm 2008-08-07 added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;
2008-08-07 wenzelm 2008-08-07 parse_token: use Syntax.read_token, pass full position information;
2008-08-07 wenzelm 2008-08-07 tuned;
2008-08-07 wenzelm 2008-08-07 map_default: more explicit scope;
2008-08-07 wenzelm 2008-08-07 datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07 wenzelm 2008-08-07 simplified Antiquote signature;
2008-08-07 wenzelm 2008-08-07 more precise positions due to SymbolsPos.implode_delim; added source' for SymbolPos.T;
2008-08-07 wenzelm 2008-08-07 simplified Antiq: regular SymbolPos.text with position; renamed read_arguments to read_antiq; tuned;
2008-08-07 wenzelm 2008-08-07 renamed SymbolPos.scan_position to SymbolPos.scan_pos; implode/explode: explicit type text = string; added implode_delim; explode: Position.reset_range;
2008-08-07 wenzelm 2008-08-07 only increment column if valid; more robust handling of invalid entries; clarified line/line_file: no column here; added start = (1, 1); added reset_range; tuned;
2008-08-07 wenzelm 2008-08-07 install_pp Position.T;
2008-08-07 wenzelm 2008-08-07 Position.start;
2008-08-07 wenzelm 2008-08-07 SymbolPos.explode;
2008-08-07 wenzelm 2008-08-07 improved position handling due to SymbolPos.T;
2008-08-07 wenzelm 2008-08-07 improved position handling due to SymbolPos.T; SymbolPos.scan_comment; tuned;
2008-08-07 wenzelm 2008-08-07 Antiquote.read/read_arguments;
2008-08-07 wenzelm 2008-08-07 updated type of nested sources;
2008-08-07 wenzelm 2008-08-07 improved position handling due to SymbolPos.T; SymbolPos.scan_comment_body; tuned;
2008-08-07 wenzelm 2008-08-07 adapted Scan.extend_lexicon/merge_lexicons;
2008-08-07 wenzelm 2008-08-07 renamed scan_antiquotes to read; renamed scan_arguments to read_arguments; improved position handling due to SymbolPos.T; tuned;
2008-08-07 wenzelm 2008-08-07 export not_eof;
2008-08-07 wenzelm 2008-08-07 reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-07 wenzelm 2008-08-07 advance: single argument (again); added range; tuned;
2008-08-07 wenzelm 2008-08-07 Symbols with explicit position information.
2008-08-07 wenzelm 2008-08-07 added General/symbol_pos.ML;
2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-06 nipkow 2008-08-06 added lemma
2008-08-06 wenzelm 2008-08-06 made SML/NJ happy;
2008-08-06 berghofe 2008-08-06 Reverted last change, since it caused incompatibilities.
2008-08-06 wenzelm 2008-08-06 fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
2008-08-06 wenzelm 2008-08-06 T.end_position_of; tuned;
2008-08-06 wenzelm 2008-08-06 adapted Antiq;
2008-08-06 wenzelm 2008-08-06 parse_sort/typ/term/prop: report markup;
2008-08-06 wenzelm 2008-08-06 sort/typ/term/prop: inner_syntax markup encodes original source position; added typ/term/prop_group (without inner_syntax markup);
2008-08-06 wenzelm 2008-08-06 removed obsolete range_of (already included in position); added end_position_of; replaced scan_string by scan_quoted (which keeps quotes and includes alt_string as well); misc tuning;
2008-08-06 wenzelm 2008-08-06 report markup;
2008-08-06 wenzelm 2008-08-06 Antiq: inner vs. outer position; scan_antiq: use T.scan_quoted;
2008-08-06 wenzelm 2008-08-06 of_properties: observe Markup.position_properties';
2008-08-06 wenzelm 2008-08-06 added position_properties'; renamed prop to proposition; added attribute, method;
2008-08-05 wenzelm 2008-08-05 token: maintain of source, which retains original position information; removed count/counted, advance position via scanned source;
2008-08-05 wenzelm 2008-08-05 moved OuterLex.count here;
2008-08-05 wenzelm 2008-08-05 improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-05 wenzelm 2008-08-05 advance: operate on symbol list (less overhead);