1 (* Title: src/Tools/isac/BridgeJEdit/Calculation.thy
2 Author: Walther Neuper, JKU Linz
3 (c) due to copyright terms
5 Outer syntax for Isabelle/Isac's Calculation.
10 (**) "~~/src/Tools/isac/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*)
11 (** )"~~/src/Tools/isac/MathEngine/MathEngine" ( *activate after devel.of BridgeJEdit*)
12 (**) "HOL-SPARK.SPARK" (*remove after devel.of BridgeJEdit*)
14 "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)
15 and "Problem" :: thy_decl (* root-problem + recursively in Solution;
16 "spark_vc" :: thy_goal *)
17 and "Specification" "Model" "References" "Solution" (* structure only *)
18 and "Given" "Find" "Relate" :: prf_chain (* await input of term *)
19 and "Where" (* only output, preliminarily *)
20 and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
21 and "RProblem" "RMethod" (* await input of string list *)
22 "Tactic" (* optional for each step 0..end of calculation *)
25 (**)ML_file parseC.sml(**)
26 (**)ML_file preliminary.sml(**)
29 section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
31 subsection \<open>code for Problem\<close>
33 Again, we copy code from spark_vc into Calculation.thy and
34 add functionality for Problem
35 such that the code keeps running during adaption from spark_vc to Problem.
40 subsubsection \<open>cp from Pure.thy\<close>
44 val facts = Parse.and_list1 Parse.thms1;
45 facts: (Facts.ref * Token.src list) list list parser;
48 (writeln "####-## from parser";
49 Parse.$$$ ":" |-- Parse.and_list1 Parse.thms1)(** ) --| Parse.$$$ "Where"( **);
50 facts: (Facts.ref * Token.src list) list list parser;
56 subsubsection \<open>TODO\<close>
62 section \<open>setup command_keyword \<close>
66 Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
67 (Resources.provide_parse_files "Example" -- Parse.parname
68 >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK: test independent from session Isac*)
69 (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)));
72 Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
73 "start a Specification, either from scratch or from preceding 'Example'"
74 (ParseC.problem >> Preliminary.prove_vc);
76 Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;
77 SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
79 \<close> ML \<open> (*-----------------------------------------------------------------------------------*)
81 Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
82 (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
84 Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find item to the Model of a Specification"
85 (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
87 Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"
88 (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
94 subsection \<open>test runs with Example\<close>
96 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
97 (*(1) outcomment before creating session Isac* )
99 (*makes Outer_Syntax..Problem run; Isac code is just added..*)
100 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
102 ( *(2) outcomment before creating session Isac* )
103 Problem ("Biegelinie", ["Biegelinien"]) (*procedure_g_c_d_4 .."Problem" adds to SPARK*)
107 Given: "Traegerlaenge "(*,*) "Streckenlast "
108 Where: "q_0 ist_integrierbar_auf {| 0, L |}"(*,*) "0 < L"
110 Relate: "Randbedingungen "
121 compare click on above Given: "Traegerlaenge ", "Streckenlast "
122 with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
125 subsection \<open><Output> BY CLICK ON Problem..Solution\<close>
127 Comparison of the two subsections below:
128 (1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:
129 ((WHILE click ON Example SHOWS NO ERROR))
130 # headline = ..(1) == (2) ..PARSED + Specification
131 # i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
132 # o_model = COMPLETE WITH 7 ELEMENTS ..FROM Example
133 # refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References
135 (2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:
136 ((WHILE click ON Example SHOWS !!! ERROR))
137 # headline = ..(1) == (2) ..PARSED + Specification
138 # i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
139 # o_model = [] ..NO Example
140 # refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"]) ..FROM headline ONLY
143 subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>
145 {a = "//--- Spark_Commands.prove_vc", headline =
146 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
147 ((((("Specification", ":"),
148 ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
151 ["<markup>", "<markup>"]),
158 (("References", ":"),
159 (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
163 "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
164 {a = "prove_vc", i_model =
165 [(0, [], false, "#Given",
166 Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
167 (0, [], false, "#Given",
168 Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
169 (0, [], false, "#Find",
170 Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
171 (Const ("empty", "??.'a"), []))),
172 (0, [], false, "#Relate",
173 Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
174 (Const ("empty", "??.'a"), [])))],
176 [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
177 (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
178 (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
179 [Free ("y", "real \<Rightarrow> real")]),
180 (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
181 [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
182 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $
183 Free ("0", "real")) $
184 Const ("List.list.Nil", "bool list"),
185 Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
186 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $
187 Free ("0", "real")) $
188 Const ("List.list.Nil", "bool list"),
189 Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
190 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
191 (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
192 Const ("List.list.Nil", "bool list"),
193 Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
194 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
195 (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
196 Const ("List.list.Nil", "bool list")]),
197 (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
198 (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
199 [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $
200 Const ("List.list.Nil", "real list"),
201 Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $
202 Const ("List.list.Nil", "real list"),
203 Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $
204 Const ("List.list.Nil", "real list"),
205 Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $
206 Const ("List.list.Nil", "real list")]),
207 (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
208 [Free ("dy", "real \<Rightarrow> real")])],
210 ("Biegelinie", ["Biegelinien"],
211 ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
212 ### Proof_Context.gen_fixes
213 ### Proof_Context.gen_fixes
214 ### Proof_Context.gen_fixes
215 ### Syntax_Phases.check_terms
216 ### Syntax_Phases.check_typs
217 ### Syntax_Phases.check_typs
218 ### Syntax_Phases.check_typs
219 ## calling Output.report
220 #### Syntax_Phases.check_props
221 ### Syntax_Phases.check_terms
222 ### Syntax_Phases.check_typs
223 ### Syntax_Phases.check_typs
224 ## calling Output.report
225 #### Syntax_Phases.check_props
226 ### Syntax_Phases.check_terms
227 ### Syntax_Phases.check_typs
228 ### Syntax_Phases.check_typs
229 ## calling Output.report
230 #### Syntax_Phases.check_props
231 ### Syntax_Phases.check_terms
232 ### Syntax_Phases.check_typs
233 ### Syntax_Phases.check_typs
234 ## calling Output.report
235 #### Syntax_Phases.check_props
236 ### Syntax_Phases.check_terms
237 ### Syntax_Phases.check_typs
238 ### Syntax_Phases.check_typs
239 ## calling Output.report
240 #### Syntax_Phases.check_props
241 ### Syntax_Phases.check_terms
242 ### Syntax_Phases.check_typs
243 ### Syntax_Phases.check_typs
244 ## calling Output.report
245 #### Syntax_Phases.check_props
246 ### Syntax_Phases.check_terms
247 ### Syntax_Phases.check_typs
248 ### Syntax_Phases.check_typs
249 ## calling Output.report
250 #### Syntax_Phases.check_props
251 ### Syntax_Phases.check_terms
252 ### Syntax_Phases.check_typs
253 ### Syntax_Phases.check_typs
254 ## calling Output.report
255 #### Syntax_Phases.check_props
256 ### Syntax_Phases.check_terms
257 ### Syntax_Phases.check_typs
258 ### Syntax_Phases.check_typs
259 ## calling Output.report
260 #### Syntax_Phases.check_props
261 ### Syntax_Phases.check_terms
262 ### Syntax_Phases.check_typs
263 ### Syntax_Phases.check_typs
264 ## calling Output.report
265 #### Syntax_Phases.check_props
266 ### Syntax_Phases.check_terms
267 ### Syntax_Phases.check_typs
268 ### Syntax_Phases.check_typs
269 ## calling Output.report
270 #### Syntax_Phases.check_props
271 ### Syntax_Phases.check_terms
272 ### Syntax_Phases.check_typs
273 ### Syntax_Phases.check_typs
274 ## calling Output.report
275 #### Syntax_Phases.check_props
276 ### Syntax_Phases.check_terms
277 ### Syntax_Phases.check_typs
278 ### Syntax_Phases.check_typs
279 ## calling Output.report
280 #### Syntax_Phases.check_props
281 ### Syntax_Phases.check_terms
282 ### Syntax_Phases.check_typs
283 ### Syntax_Phases.check_typs
284 ## calling Output.report
285 #### Syntax_Phases.check_props
286 ### Syntax_Phases.check_terms
287 ### Syntax_Phases.check_typs
288 ### Syntax_Phases.check_typs
289 ## calling Output.report
290 #### Syntax_Phases.check_props
291 ### Syntax_Phases.check_terms
292 ### Syntax_Phases.check_typs
293 ### Syntax_Phases.check_typs
294 ## calling Output.report
295 #### Syntax_Phases.check_props
296 ### Syntax_Phases.check_terms
297 ### Syntax_Phases.check_typs
298 ### Syntax_Phases.check_typs
299 ## calling Output.report
300 #### Syntax_Phases.check_props
301 ### Syntax_Phases.check_terms
302 ### Syntax_Phases.check_typs
303 ### Syntax_Phases.check_typs
304 ## calling Output.report
305 #### Syntax_Phases.check_props
306 ### Syntax_Phases.check_terms
307 ### Syntax_Phases.check_typs
308 ### Syntax_Phases.check_typs
309 ## calling Output.report
310 #### Syntax_Phases.check_props
311 ### Syntax_Phases.check_terms
312 ### Syntax_Phases.check_typs
313 ### Syntax_Phases.check_typs
314 ## calling Output.report
315 #### Syntax_Phases.check_props
316 ### Syntax_Phases.check_terms
317 ### Syntax_Phases.check_typs
318 ### Syntax_Phases.check_typs
319 ## calling Output.report
320 #### Syntax_Phases.check_props
321 ### Syntax_Phases.check_terms
322 ### Syntax_Phases.check_typs
323 ### Syntax_Phases.check_typs
324 ## calling Output.report
325 #### Syntax_Phases.check_props
326 ### Syntax_Phases.check_terms
327 ### Syntax_Phases.check_typs
328 ### Syntax_Phases.check_typs
329 ### Syntax_Phases.check_typs
330 ## calling Output.report
331 #### Syntax_Phases.check_props
332 ### Syntax_Phases.check_terms
333 ### Syntax_Phases.check_typs
334 ### Syntax_Phases.check_typs
335 ### Syntax_Phases.check_typs
336 ## calling Output.report
337 ### Syntax_Phases.check_terms
338 ### Syntax_Phases.check_typs
339 ### Syntax_Phases.check_typs
340 ### Syntax_Phases.check_typs
341 ## calling Output.report
342 ### Syntax_Phases.check_terms
343 ### Syntax_Phases.check_typs
344 ### Syntax_Phases.check_typs
345 ### Syntax_Phases.check_typs
346 ## calling Output.report
347 ### Syntax_Phases.check_terms
348 ### Syntax_Phases.check_typs
349 ### Syntax_Phases.check_typs
350 ### Syntax_Phases.check_typs
351 ## calling Output.report
352 ### Syntax_Phases.check_terms
353 ### Syntax_Phases.check_typs
354 ### Syntax_Phases.check_typs
355 ### Syntax_Phases.check_typs
356 ## calling Output.report
357 ### Syntax_Phases.check_terms
358 ### Syntax_Phases.check_typs
359 ### Syntax_Phases.check_typs
360 ### Syntax_Phases.check_typs
361 ## calling Output.report
362 ### Proof_Context.gen_fixes
363 ### Proof_Context.gen_fixes
366 subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>
368 {a = "//--- Spark_Commands.prove_vc", headline =
369 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
370 ((((("Specification", ":"),
371 ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
374 ["<markup>", "<markup>"]),
381 (("References", ":"),
382 (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
387 {a = "prove_vc", i_model =
388 [(0, [], false, "#Given",
389 Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
390 (0, [], false, "#Given",
391 Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
392 (0, [], false, "#Find",
393 Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
394 (Const ("empty", "??.'a"), []))),
395 (0, [], false, "#Relate",
396 Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
397 (Const ("empty", "??.'a"), [])))],
398 o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}
399 ### Proof_Context.gen_fixes
400 ### Proof_Context.gen_fixes
401 ### Proof_Context.gen_fixes
402 ### Syntax_Phases.check_terms
403 ### Syntax_Phases.check_typs
404 ### Syntax_Phases.check_typs
405 ### Syntax_Phases.check_typs
406 ## calling Output.report
407 #### Syntax_Phases.check_props
408 ### Syntax_Phases.check_terms
409 ### Syntax_Phases.check_typs
410 ### Syntax_Phases.check_typs
411 ## calling Output.report
412 #### Syntax_Phases.check_props
413 ### Syntax_Phases.check_terms
414 ### Syntax_Phases.check_typs
415 ### Syntax_Phases.check_typs
416 ## calling Output.report
417 #### Syntax_Phases.check_props
418 ### Syntax_Phases.check_terms
419 ### Syntax_Phases.check_typs
420 ### Syntax_Phases.check_typs
421 ## calling Output.report
422 #### Syntax_Phases.check_props
423 ### Syntax_Phases.check_terms
424 ### Syntax_Phases.check_typs
425 ### Syntax_Phases.check_typs
426 ## calling Output.report
427 #### Syntax_Phases.check_props
428 ### Syntax_Phases.check_terms
429 ### Syntax_Phases.check_typs
430 ### Syntax_Phases.check_typs
431 ## calling Output.report
432 #### Syntax_Phases.check_props
433 ### Syntax_Phases.check_terms
434 ### Syntax_Phases.check_typs
435 ### Syntax_Phases.check_typs
436 ## calling Output.report
437 #### Syntax_Phases.check_props
438 ### Syntax_Phases.check_terms
439 ### Syntax_Phases.check_typs
440 ### Syntax_Phases.check_typs
441 ## calling Output.report
442 #### Syntax_Phases.check_props
443 ### Syntax_Phases.check_terms
444 ### Syntax_Phases.check_typs
445 ### Syntax_Phases.check_typs
446 ## calling Output.report
447 #### Syntax_Phases.check_props
448 ### Syntax_Phases.check_terms
449 ### Syntax_Phases.check_typs
450 ### Syntax_Phases.check_typs
451 ## calling Output.report
452 #### Syntax_Phases.check_props
453 ### Syntax_Phases.check_terms
454 ### Syntax_Phases.check_typs
455 ### Syntax_Phases.check_typs
456 ## calling Output.report
457 #### Syntax_Phases.check_props
458 ### Syntax_Phases.check_terms
459 ### Syntax_Phases.check_typs
460 ### Syntax_Phases.check_typs
461 ## calling Output.report
462 #### Syntax_Phases.check_props
463 ### Syntax_Phases.check_terms
464 ### Syntax_Phases.check_typs
465 ### Syntax_Phases.check_typs
466 ## calling Output.report
467 #### Syntax_Phases.check_props
468 ### Syntax_Phases.check_terms
469 ### Syntax_Phases.check_typs
470 ### Syntax_Phases.check_typs
471 ## calling Output.report
472 #### Syntax_Phases.check_props
473 ### Syntax_Phases.check_terms
474 ### Syntax_Phases.check_typs
475 ### Syntax_Phases.check_typs
476 ## calling Output.report
477 #### Syntax_Phases.check_props
478 ### Syntax_Phases.check_terms
479 ### Syntax_Phases.check_typs
480 ### Syntax_Phases.check_typs
481 ## calling Output.report
482 #### Syntax_Phases.check_props
483 ### Syntax_Phases.check_terms
484 ### Syntax_Phases.check_typs
485 ### Syntax_Phases.check_typs
486 ## calling Output.report
487 #### Syntax_Phases.check_props
488 ### Syntax_Phases.check_terms
489 ### Syntax_Phases.check_typs
490 ### Syntax_Phases.check_typs
491 ## calling Output.report
492 #### Syntax_Phases.check_props
493 ### Syntax_Phases.check_terms
494 ### Syntax_Phases.check_typs
495 ### Syntax_Phases.check_typs
496 ## calling Output.report
497 #### Syntax_Phases.check_props
498 ### Syntax_Phases.check_terms
499 ### Syntax_Phases.check_typs
500 ### Syntax_Phases.check_typs
501 ## calling Output.report
502 #### Syntax_Phases.check_props
503 ### Syntax_Phases.check_terms
504 ### Syntax_Phases.check_typs
505 ### Syntax_Phases.check_typs
506 ## calling Output.report
507 #### Syntax_Phases.check_props
508 ### Syntax_Phases.check_terms
509 ### Syntax_Phases.check_typs
510 ### Syntax_Phases.check_typs
511 ## calling Output.report
512 #### Syntax_Phases.check_props
513 ### Syntax_Phases.check_terms
514 ### Syntax_Phases.check_typs
515 ### Syntax_Phases.check_typs
516 ### Syntax_Phases.check_typs
517 ## calling Output.report
518 #### Syntax_Phases.check_props
519 ### Syntax_Phases.check_terms
520 ### Syntax_Phases.check_typs
521 ### Syntax_Phases.check_typs
522 ### Syntax_Phases.check_typs
523 ## calling Output.report
524 ### Syntax_Phases.check_terms
525 ### Syntax_Phases.check_typs
526 ### Syntax_Phases.check_typs
527 ### Syntax_Phases.check_typs
528 ## calling Output.report
529 ### Syntax_Phases.check_terms
530 ### Syntax_Phases.check_typs
531 ### Syntax_Phases.check_typs
532 ### Syntax_Phases.check_typs
533 ## calling Output.report
534 ### Syntax_Phases.check_terms
535 ### Syntax_Phases.check_typs
536 ### Syntax_Phases.check_typs
537 ### Syntax_Phases.check_typs
538 ## calling Output.report
539 ### Syntax_Phases.check_terms
540 ### Syntax_Phases.check_typs
541 ### Syntax_Phases.check_typs
542 ### Syntax_Phases.check_typs
543 ## calling Output.report
544 ### Syntax_Phases.check_terms
545 ### Syntax_Phases.check_typs
546 ### Syntax_Phases.check_typs
547 ### Syntax_Phases.check_typs
548 ## calling Output.report
549 ### Proof_Context.gen_fixes
550 ### Proof_Context.gen_fixes
553 section \<open>Notes: adapt spark_vc to Problem using Naproche as model\<close>
555 subsection \<open>survey on steps of investigation\<close>
557 We stopped step 3.4 going down from Outer_Syntax.local_theory_to_proof into proof.
558 Now we go the other way: Naproche checks the input via the Isabelle/server
559 and outputs highlighting, semantic annotations and errors via PIDE ---
560 and we investigate the output.
562 Investigation of Naproche showed, that annotations are ONLY sent bY
563 Output.report: string list -> unit, where string holds markup.
564 For Output.report @ {print} is NOT available, so we trace all respective CALLS.
565 However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4",
566 so tracing is done by writeln (which breaks build between Main and Complex_Main
567 by writing longer strings, see Pure/General/output.ML).
569 Tracing is implemented in (1) Isabelle_Naproche and in (2) isabisac in parallel;
570 (1) requires only Pure, thus is built quicker, but does NOT handle proofs within ML
571 (2) requires HOL.SPARK, there is full proof handling, but this is complex.
573 Tracing the calls of Output.report shows some properties of handling proofs,
574 see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
577 end(* HERE SEVERAL ERRORS SHOW UP, CAUSED FROM ABOVE..
578 "(1) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..
579 Bad context for command "end"\<^here> -- using reset state
580 Found the end of the theory, but the last SPARK environment is still open.
581 "(2) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..
583 Bad context for command "end"\<^here> -- using reset state*)