Thu, 16 Feb 2023 16:20:10 +0100 wneuper tuned
Thu, 16 Feb 2023 15:53:10 +0100 wneuper PIDE turn 2: prepare for stepwise input
Wed, 15 Feb 2023 15:56:09 +0100 wneuper PIDE turn 1: model's terms show syntax error
Mon, 13 Feb 2023 15:50:53 +0100 wneuper PIDE turn 0: setup for Outer_Syntax.command \<^command_keyword>?Test_Example?
Mon, 13 Feb 2023 15:37:41 +0100 wneuper eliminate SPARK as a model for using Isabelle/PIDE
Mon, 13 Feb 2023 09:54:34 +0100 wneuper tuned
Sun, 12 Feb 2023 14:06:11 +0100 wneuper one more TODO
Sun, 12 Feb 2023 12:44:25 +0100 wneuper move code from LibraryC to approptiate structures
Wed, 08 Feb 2023 08:59:37 +0100 wneuper rollback
Wed, 08 Feb 2023 07:51:39 +0100 wneuper remove accomplished TODOs
Tue, 07 Feb 2023 18:32:58 +0100 wneuper improve previous changeset
Tue, 07 Feb 2023 18:05:15 +0100 wneuper unify ctxt for ERROR
Tue, 07 Feb 2023 17:43:16 +0100 wneuper eliminate use of Thy_Info 24: finished
Tue, 07 Feb 2023 17:25:09 +0100 wneuper eliminate use of Thy_Info 23: ThyC.get_theory ctxt is mandadory
Sat, 04 Feb 2023 17:00:25 +0100 wneuper eliminate use of Thy_Info 22: eliminate UnparseC.term, rename "_in_ctxt" -> ""
Sat, 04 Feb 2023 16:49:08 +0100 wneuper rollback
Sat, 04 Feb 2023 16:20:45 +0100 wneuper eliminate use of Thy_Info 21: replace Unparse.term, TermC.unparse_ERROR for far off ctxt
Sat, 04 Feb 2023 11:21:56 +0100 wneuper eliminate use of Thy_Info 20: cleanup Subst.*, detect design flaw in fun eval_*
Sat, 04 Feb 2023 09:47:27 +0100 wneuper eliminate use of Thy_Info 19: some more uses of UnparseC.term_in_ctxt
Fri, 03 Feb 2023 15:26:19 +0100 wneuper eliminate use of Thy_Info 18: UnparseC.terms_to_strings --> asms_test
Fri, 03 Feb 2023 12:56:05 +0100 wneuper eliminate use of Thy_Info 17: UnparseC.term_short --> asms_test
Fri, 03 Feb 2023 12:05:30 +0100 wneuper eliminate use of Thy_Info 16: eliminate UnparseC.terms in src/*, too
Tue, 31 Jan 2023 16:29:53 +0100 wneuper eliminate use of Thy_Info 15: UnparseC.terms --> terms_in_ctxt, only test/*
Tue, 31 Jan 2023 12:47:11 +0100 wneuper eliminate use of Thy_Info 14: UnparseC.term_opt ctxt
Tue, 31 Jan 2023 12:29:42 +0100 wneuper eliminate use of Thy_Info 13: eliminate UnparseC.term in test/
Tue, 31 Jan 2023 11:23:16 +0100 wneuper cleanup parse #7: eliminate TermC.parseNEW*; cleanup finished
Tue, 31 Jan 2023 10:49:17 +0100 wneuper cleanup parse #6: eliminate TermC.parseNEW
Mon, 30 Jan 2023 12:38:17 +0100 wneuper cleanup parse #5: eliminate TermC.parse_patt
Mon, 30 Jan 2023 12:11:40 +0100 wneuper cleanup parse #4: eliminate TermC.parse
Mon, 30 Jan 2023 09:47:18 +0100 wneuper cleanup parse #3: final functions inb ParseC
Sun, 29 Jan 2023 14:31:56 +0100 wneuper cleanup parse #2: repair error hidden by parse NONE in I_Model.check_single
Sat, 28 Jan 2023 13:21:39 +0100 wneuper cleanup parse #1: start eliminate parseNEW
Thu, 26 Jan 2023 19:02:41 +0100 wneuper cleanup
Thu, 26 Jan 2023 18:58:17 +0100 wneuper renaming
Thu, 26 Jan 2023 18:54:25 +0100 wneuper use exclusively some new *.to_string ctxt
Thu, 26 Jan 2023 13:31:07 +0100 wneuper use exclusively new ContextC.build_while_parsing
Wed, 25 Jan 2023 18:35:02 +0100 wneuper use exclusively new O_Model.init
Wed, 25 Jan 2023 17:51:52 +0100 wneuper use exclusively new Step_Specify.initialise / initialise'
Wed, 25 Jan 2023 15:52:33 +0100 wneuper ContextC.build_while_parsing, improves O_Model.init_PIDE
Wed, 11 Jan 2023 11:38:01 +0100 wneuper eliminate use of Thy_Info 12: TermC partially
Wed, 11 Jan 2023 09:23:18 +0100 wneuper eliminate use of Thy_Info 12: prep.arg. ctxt in TermC, UnparseC
Wed, 11 Jan 2023 06:06:12 +0100 wneuper eliminate use of Thy_Info 11: arg. ctxt for ThmC.string_of_thm/s
Tue, 10 Jan 2023 17:07:53 +0100 wneuper eliminate use of Thy_Info 10: arg. ctxt for Rule.to_string finished
Tue, 10 Jan 2023 10:01:05 +0100 wneuper eliminate use of Thy_Info 9: arg. ctxt for Rule.to_string, Istate.to_string
Mon, 09 Jan 2023 16:40:54 +0100 wneuper eliminate use of Thy_Info 8: arg. ctxt for Rule.to_string, partially
Mon, 09 Jan 2023 16:11:17 +0100 wneuper eliminate use of Thy_Info 6: improved ThmC.*_sym_rule
Sun, 08 Jan 2023 17:26:00 +0100 wneuper eliminate use of Thy_Info 6: improve ctxt in fetchProposedTactic, Error_Pattern, etc
Sun, 08 Jan 2023 16:19:31 +0100 wneuper eliminate use of Thy_Info 5: ThyC.get_theory in Error_Pattern, Kernel
Sun, 08 Jan 2023 12:33:27 +0100 wneuper eliminate use of Thy_Info 4: ThyC.get_theory in Step_Solve, Fetch_Tacs
Sun, 08 Jan 2023 10:30:58 +0100 wneuper eliminate use of Thy_Info 3> improved LItool.tac_from_prog
Fri, 06 Jan 2023 15:40:45 +0100 wneuper eliminate use of Thy_Info 2: ThyC.get_theory in Math_Engine
Fri, 06 Jan 2023 15:06:40 +0100 wneuper eliminate use of Thy_Info 1: ThyC.get_theory in Specify_Step, Specify, Step_Specify
Fri, 06 Jan 2023 11:43:50 +0100 wneuper polished
Fri, 06 Jan 2023 11:32:57 +0100 wneuper eliminate thy-hierarchy 5, end: remove Thy_Write
Fri, 06 Jan 2023 10:50:33 +0100 wneuper eliminate thy-hierarchy 4: remove Thy_Read
Fri, 06 Jan 2023 10:33:16 +0100 wneuper eliminate thy-hierarchy 3: shift (part of) metadata to ThyC
Fri, 06 Jan 2023 09:55:35 +0100 wneuper shift add_errpats to respective theory
Fri, 06 Jan 2023 08:33:18 +0100 wneuper eliminate thy-hierarchy 2: Error_Pattern.from_store independent
Fri, 06 Jan 2023 08:04:36 +0100 wneuper eliminate thy-hierarchy 1: Error_Pattern.fill_from_store independent from..
Thu, 22 Dec 2022 17:06:19 +0100 wneuper make Minisubplb/800-append-on-Frm.sml independent from Thy_Info