# HG changeset patch # User wenzelm # Date 1243107634 -7200 # Node ID 5c1aca930404b93d68935b3f553fb2c0d4dc852b # Parent 2a1f5c87ac2884300f04a0a5841e90019de7f786 proper indentation; diff -r 2a1f5c87ac28 -r 5c1aca930404 src/Pure/Isar/isar_document.scala --- a/src/Pure/Isar/isar_document.scala Sat May 23 21:31:07 2009 +0200 +++ b/src/Pure/Isar/isar_document.scala Sat May 23 21:40:34 2009 +0200 @@ -31,7 +31,7 @@ def begin_document(id: Document_ID, path: String) { output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " + - IsabelleSyntax.encode_string(path)) + IsabelleSyntax.encode_string(path)) } def end_document(id: Document_ID) {