xtest-to-coding.sh
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 19 Jan 2017 10:35:39 +0100
changeset 59296 76c65580077b
parent 59295 3c894c3db67d
child 59316 3a60188d9cc3
permissions -rwxr-xr-x
separate structure CTnavi : CALC_TREE_NAVIGATION

Note: separation not yet perfect: 3 "duplicates in ctree-basic.sml"
wneuper@59295
     1
# switches isac from test-mode to coding-mode:
wneuper@59295
     2
# this closes signatures as much as possible for coding.
wneuper@59295
     3
wneuper@59295
     4
cd src/Tools/isac
wneuper@59295
     5
find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
wneuper@59295
     6
find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
wneuper@59295
     7
cd ../../../
wneuper@59296
     8
./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &