ztest-to-coding.sh
author Walther Neuper <wneuper@ist.tugraz.at>
Sat, 24 Mar 2018 14:34:47 +0100
changeset 59412 3bd4be5666de
parent 59375 946735bfc15a
child 59429 c0fe04973189
permissions -rwxr-xr-x
Celem: Test_Isac works completely
wneuper@59316
     1
# switches isac from test-mode to coding-mode:
wneuper@59320
     2
# this closes signatures as much as possible for coding.
wneuper@59316
     3
wneuper@59316
     4
cd src/Tools/isac
wneuper@59316
     5
find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
wneuper@59316
     6
find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
wneuper@59320
     7
cd ../../../  # go back to ~~/.
wneuper@59320
     8
wneuper@59320
     9
# immediately go to correcting code in Interpret/
wneuper@59412
    10
#./bin/isabelle jedit src/Tools/isac/ProgLang/ProgLang.thy &
wneuper@59412
    11
./bin/isabelle jedit src/Tools/isac/Isac_Protocol.thy &