Tue, 23 May 2023 08:34:53 +0200 |
wneuper |
prepare 2: adapt LItool.init_pstate to I_Model with Position.T
|
changeset |
files
|
Tue, 23 May 2023 07:56:29 +0200 |
wneuper |
rollback
|
changeset |
files
|
Sat, 29 Apr 2023 16:47:59 +0200 |
wneuper |
prepare 1 PIDE turn 11: eliminate P_Spec.parseitm used by I_Model.Par
|
changeset |
files
|
Sat, 29 Apr 2023 15:53:37 +0200 |
wneuper |
add missing I_Model.OLD_to_TEST to sig
|
changeset |
files
|
Wed, 05 Apr 2023 17:46:25 +0200 |
wneuper |
repair Test_Isac (remove one flaw)
|
changeset |
files
|
Tue, 04 Apr 2023 10:54:12 +0200 |
wneuper |
PIDE turn 10> new handling of variants, Pre_Conds.check_OLD/_TEST, I_Model.is_complete_OLD/_TEST
|
changeset |
files
|
Fri, 31 Mar 2023 12:07:52 +0200 |
wneuper |
//new Pre_Conds.check/_TEST breaks tests, need new signature
|
changeset |
files
|
Wed, 08 Mar 2023 17:47:07 +0100 |
wneuper |
CTbasic_TEST holds I_Model_TEST with Position.T,
|
changeset |
files
|
Tue, 07 Mar 2023 16:06:18 +0100 |
wneuper |
repair previous changeset
|
changeset |
files
|
Tue, 07 Mar 2023 15:38:23 +0100 |
wneuper |
I_Model.init_TEST provides completion as far as reasonable
|
changeset |
files
|
Sun, 05 Mar 2023 08:51:34 +0100 |
wneuper |
rename superfluous *_TEST
|
changeset |
files
|
Sat, 04 Mar 2023 19:06:00 +0100 |
wneuper |
tuned
|
changeset |
files
|
Sat, 04 Mar 2023 19:02:39 +0100 |
wneuper |
PIDE turn 9a: handle empty input correct
|
changeset |
files
|
Mon, 27 Feb 2023 09:45:29 +0100 |
wneuper |
PIDE turn 9: handle empty input, error in Test_VSCode_Example, isabelle@
|
changeset |
files
|
Fri, 24 Feb 2023 16:14:28 +0100 |
wneuper |
PIDE turn 8: reorganise Test_VSCode_Example.thy, etc
|
changeset |
files
|
Wed, 22 Feb 2023 18:40:34 +0100 |
wneuper |
add files
|
changeset |
files
|
Wed, 22 Feb 2023 18:38:56 +0100 |
wneuper |
PIDE turn 7: prepare for Template.show
|
changeset |
files
|
Tue, 21 Feb 2023 15:59:46 +0100 |
wneuper |
PIDE turn 6: feedback with Position.T in MODEL_FOR_INTERACTION
|
changeset |
files
|
Mon, 20 Feb 2023 12:51:17 +0100 |
wneuper |
correct last cs: add files etc
|
changeset |
files
|
Mon, 20 Feb 2023 12:33:23 +0100 |
wneuper |
PIDE turn 5: more structure
|
changeset |
files
|
Sun, 19 Feb 2023 13:03:54 +0100 |
wneuper |
PIDE turn 4: I_Model.init requires other datatype feedback
|
changeset |
files
|
Sun, 19 Feb 2023 10:29:58 +0100 |
wneuper |
PIDE turn 3: hints for input format of terms in Model
|
changeset |
files
|
Thu, 16 Feb 2023 16:20:10 +0100 |
wneuper |
tuned
|
changeset |
files
|
Thu, 16 Feb 2023 15:53:10 +0100 |
wneuper |
PIDE turn 2: prepare for stepwise input
|
changeset |
files
|
Wed, 15 Feb 2023 15:56:09 +0100 |
wneuper |
PIDE turn 1: model's terms show syntax error
|
changeset |
files
|
Mon, 13 Feb 2023 15:50:53 +0100 |
wneuper |
PIDE turn 0: setup for Outer_Syntax.command \<^command_keyword>?Test_Example?
|
changeset |
files
|
Mon, 13 Feb 2023 15:37:41 +0100 |
wneuper |
eliminate SPARK as a model for using Isabelle/PIDE
|
changeset |
files
|
Mon, 13 Feb 2023 09:54:34 +0100 |
wneuper |
tuned
|
changeset |
files
|
Sun, 12 Feb 2023 14:06:11 +0100 |
wneuper |
one more TODO
|
changeset |
files
|
Sun, 12 Feb 2023 12:44:25 +0100 |
wneuper |
move code from LibraryC to approptiate structures
|
changeset |
files
|
Wed, 08 Feb 2023 08:59:37 +0100 |
wneuper |
rollback
|
changeset |
files
|
Wed, 08 Feb 2023 07:51:39 +0100 |
wneuper |
remove accomplished TODOs
|
changeset |
files
|
Tue, 07 Feb 2023 18:32:58 +0100 |
wneuper |
improve previous changeset
|
changeset |
files
|
Tue, 07 Feb 2023 18:05:15 +0100 |
wneuper |
unify ctxt for ERROR
|
changeset |
files
|
Tue, 07 Feb 2023 17:43:16 +0100 |
wneuper |
eliminate use of Thy_Info 24: finished
|
changeset |
files
|
Tue, 07 Feb 2023 17:25:09 +0100 |
wneuper |
eliminate use of Thy_Info 23: ThyC.get_theory ctxt is mandadory
|
changeset |
files
|
Sat, 04 Feb 2023 17:00:25 +0100 |
wneuper |
eliminate use of Thy_Info 22: eliminate UnparseC.term, rename "_in_ctxt" -> ""
|
changeset |
files
|
Sat, 04 Feb 2023 16:49:08 +0100 |
wneuper |
rollback
|
changeset |
files
|
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
|
changeset |
files
|
Sat, 04 Feb 2023 11:21:56 +0100 |
wneuper |
eliminate use of Thy_Info 20: cleanup Subst.*, detect design flaw in fun eval_*
|
changeset |
files
|
Sat, 04 Feb 2023 09:47:27 +0100 |
wneuper |
eliminate use of Thy_Info 19: some more uses of UnparseC.term_in_ctxt
|
changeset |
files
|
Fri, 03 Feb 2023 15:26:19 +0100 |
wneuper |
eliminate use of Thy_Info 18: UnparseC.terms_to_strings --> asms_test
|
changeset |
files
|
Fri, 03 Feb 2023 12:56:05 +0100 |
wneuper |
eliminate use of Thy_Info 17: UnparseC.term_short --> asms_test
|
changeset |
files
|
Fri, 03 Feb 2023 12:05:30 +0100 |
wneuper |
eliminate use of Thy_Info 16: eliminate UnparseC.terms in src/*, too
|
changeset |
files
|
Tue, 31 Jan 2023 16:29:53 +0100 |
wneuper |
eliminate use of Thy_Info 15: UnparseC.terms --> terms_in_ctxt, only test/*
|
changeset |
files
|
Tue, 31 Jan 2023 12:47:11 +0100 |
wneuper |
eliminate use of Thy_Info 14: UnparseC.term_opt ctxt
|
changeset |
files
|
Tue, 31 Jan 2023 12:29:42 +0100 |
wneuper |
eliminate use of Thy_Info 13: eliminate UnparseC.term in test/
|
changeset |
files
|
Tue, 31 Jan 2023 11:23:16 +0100 |
wneuper |
cleanup parse #7: eliminate TermC.parseNEW*; cleanup finished
|
changeset |
files
|
Tue, 31 Jan 2023 10:49:17 +0100 |
wneuper |
cleanup parse #6: eliminate TermC.parseNEW
|
changeset |
files
|
Mon, 30 Jan 2023 12:38:17 +0100 |
wneuper |
cleanup parse #5: eliminate TermC.parse_patt
|
changeset |
files
|
Mon, 30 Jan 2023 12:11:40 +0100 |
wneuper |
cleanup parse #4: eliminate TermC.parse
|
changeset |
files
|
Mon, 30 Jan 2023 09:47:18 +0100 |
wneuper |
cleanup parse #3: final functions inb ParseC
|
changeset |
files
|
Sun, 29 Jan 2023 14:31:56 +0100 |
wneuper |
cleanup parse #2: repair error hidden by parse NONE in I_Model.check_single
|
changeset |
files
|
Sat, 28 Jan 2023 13:21:39 +0100 |
wneuper |
cleanup parse #1: start eliminate parseNEW
|
changeset |
files
|
Thu, 26 Jan 2023 19:02:41 +0100 |
wneuper |
cleanup
|
changeset |
files
|
Thu, 26 Jan 2023 18:58:17 +0100 |
wneuper |
renaming
|
changeset |
files
|
Thu, 26 Jan 2023 18:54:25 +0100 |
wneuper |
use exclusively some new *.to_string ctxt
|
changeset |
files
|
Thu, 26 Jan 2023 13:31:07 +0100 |
wneuper |
use exclusively new ContextC.build_while_parsing
|
changeset |
files
|
Wed, 25 Jan 2023 18:35:02 +0100 |
wneuper |
use exclusively new O_Model.init
|
changeset |
files
|
Wed, 25 Jan 2023 17:51:52 +0100 |
wneuper |
use exclusively new Step_Specify.initialise / initialise'
|
changeset |
files
|