equal
deleted
inserted
replaced
31 Output.status (Markup.markup (Markup.assign new_id) |
31 Output.status (Markup.markup (Markup.assign new_id) |
32 (implode (map (Markup.markup_only o Markup.edit) updates))); |
32 (implode (map (Markup.markup_only o Markup.edit) updates))); |
33 val state'' = Document.execute new_id state'; |
33 val state'' = Document.execute new_id state'; |
34 in state'' end)); |
34 in state'' end)); |
35 |
35 |
|
36 val _ = |
|
37 Isabelle_Process.add_command "Isar_Document.invoke_scala" |
|
38 (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); |
|
39 |
36 end; |
40 end; |
37 |
41 |