# HG changeset patch
# User wenzelm
# Date 1348664219 -7200
# Node ID f27cb2662edaf099bb828f91cfc363eaf1482e02
# Parent  0f087257ba046d95cbc6aebe9fc63055f3435a5c
proper Symbol.decode -- especially relevant for Proof General;

diff -r 0f087257ba04 -r f27cb2662eda src/Tools/Graphview/src/frame.scala
--- a/src/Tools/Graphview/src/frame.scala	Wed Sep 26 14:55:51 2012 +0200
+++ b/src/Tools/Graphview/src/frame.scala	Wed Sep 26 14:56:59 2012 +0200
@@ -27,7 +27,7 @@
 
         args.toList match {
           case List(arg) =>
-            Model.decode_graph(YXML.parse_body(File.read(Path.explode(arg))))
+            Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
           case _ => error("Bad arguments:\n" + cat_lines(args))
         }
       }