ztest-to-coding.sh
changeset 59320 4549c6062b30
parent 59316 3a60188d9cc3
child 59375 946735bfc15a
equal deleted inserted replaced
59319:dfee1c403242 59320:4549c6062b30
     1 # switches isac from test-mode to coding-mode:
     1 # switches isac from test-mode to coding-mode:
     2 # this closes signatures as much as possible for coding;
     2 # this closes signatures as much as possible for coding.
     3 
     3 
     4 cd src/Tools/isac
     4 cd src/Tools/isac
     5 find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
     5 find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
     6 find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
     6 find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
     7 cd ../../../
     7 cd ../../../  # go back to ~~/.
       
     8 
       
     9 # immediately go to correcting code in Interpret/
     8 ./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &
    10 ./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &